Heap_List_BisimulationSpec

Value Members

1. final def !=(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

2. final def !=(arg0: Any): Boolean

   Definition Classes

   Any

3. final def ##(): Int

   Definition Classes

   AnyRef → Any

4. final def ==(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

5. final def ==(arg0: Any): Boolean

   Definition Classes

   Any

6. final def asInstanceOf[T0]: T0

   Definition Classes

   Any

7. def bisim_deleteMin(h: HeapNode, l: ListHeap): Boolean

   h ~ l implies h.

   h ~ l implies h.deleteMin ~ l.deleteMin

8. def bisim_findMin(h: HeapNode, l: ListHeap): Boolean

   h ~ l implies h.

   h ~ l implies h.findMin == l.findMin

9. def bisim_insert(h: HeapNode, l: ListHeap, e: BigInt): Boolean

   h ~ l implies h.

   h ~ l implies h.insert(e) ~ l.insert(e)

10. def bisim_merge(h1: HeapNode, h2: HeapNode, l1: ListHeap, l2: ListHeap): Boolean

    h1 ~ l1 and h2 ~ l2 implies h1.

    h1 ~ l1 and h2 ~ l2 implies h1.merge(h2) ~ l1.merge(l2)

11. def bisim_size(h: HeapNode, l: ListHeap): Boolean

    h1 ~ h2 implies h1.

    h1 ~ h2 implies h1.size == h2.size

12. def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

13. final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

14. def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

15. def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

16. final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

17. def hashCode(): Int

    Definition Classes

    AnyRef → Any

18. def insert_comm_prop(l: ListHeap, e1: BigInt, e2: BigInt): Boolean

19. final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

20. def list_insert_comm(l: List[BigInt], e1: BigInt, e2: BigInt): Boolean

    Annotations

    @induct()

21. def merge_assoc_prop(l1: ListHeap, l2: ListHeap, l3: ListHeap): Boolean

22. def merge_comm_prop(l1: ListHeap, l2: ListHeap): Boolean

23. final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

24. final def notify(): Unit

    Definition Classes

    AnyRef

25. final def notifyAll(): Unit

    Definition Classes

    AnyRef

26. final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

27. implicit def toHeap(l: List[BigInt]): ListHeap

28. implicit def toList(h: ListHeap): List[BigInt]

29. def toString(): String

    Definition Classes

    AnyRef → Any

30. final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

31. final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

32. final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )