PrimitiveDataTypeSpec

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 clone(): AnyRef

   Attributes

   protected[java.lang]

   Definition Classes

   AnyRef

   Annotations

   @throws( ... )

8. def double_add_lemma(a1: Double, a2: Double, a3: Double): Boolean

   Check that 64-bit floating-point additions are commutative and associative.

   Check that 64-bit floating-point additions are commutative and associative.

   Annotations

   @ignore()

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

   Definition Classes

   AnyRef

10. def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

11. def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

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

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

    Definition Classes

    AnyRef → Any

13. def hashCode(): Int

    Definition Classes

    AnyRef → Any

14. def int32_add_lemma(a1: Int, a2: Int, a3: Int): Boolean

    Check that 32-bit integer additions are commutative and associative.

    Check that 32-bit integer additions are commutative and associative. (Note that Leon handles overflow by wrapping, e.g., 2^{32 == -2}31.)

15. def int32_vector_add_lemma(a1: List[Int], a2: List[Int], a3: List[Int]): Boolean

    Check that point-wise additions of Int32 vectors are commutative and associative.

    Check that point-wise additions of Int32 vectors are commutative and associative. Note: Leon may take up to 30 seconds to verify this lemma on my desktop.

16. def int_vector_add_lemma(a1: List[BigInt], a2: List[BigInt], a3: List[BigInt]): Boolean

    Check that point-wise additions of mathematical integer vectors are commutative and associative.

17. def integer_add_lemma(a1: BigInt, a2: BigInt, a3: BigInt): Boolean

    Check that mathematical integer additions are commutative and associative.

18. def integer_max_lemma(a1: BigInt, a2: BigInt, a3: BigInt): Boolean

    Check that choosing maximum is commutative and associative.

19. final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

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

    Definition Classes

    AnyRef

21. final def notify(): Unit

    Definition Classes

    AnyRef

22. final def notifyAll(): Unit

    Definition Classes

    AnyRef

23. def set_union_lemma[B](a1: Set[B], a2: Set[B], a3: Set[B]): Boolean

    Check that set union operations are commutative and associative.

24. def set_vector_add_lemma[B](a1: List[Set[B]], a2: List[Set[B]], a3: List[Set[B]]): Boolean

    Check that point-wise unions of set vectors are commutative and associative.

    Check that point-wise unions of set vectors are commutative and associative.

    Annotations

    @ignore()

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

    Definition Classes

    AnyRef

26. def toString(): String

    Definition Classes

    AnyRef → Any

27. final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )