diff --git a/testcases/verification/math/RationalProps.scala b/testcases/verification/math/RationalProps.scala index 60d30a6c69d361ef3185e572357f8fcb52708227..aec07246e2e8f76b3a054cd202e7beaae32f3da5 100644 --- a/testcases/verification/math/RationalProps.scala +++ b/testcases/verification/math/RationalProps.scala @@ -66,4 +66,24 @@ object RationalProps { require(p.isRational && q.isRational && q.nonZero) ((p / q) * q) ~ p } holds + + + /* + * properties of equivalence + */ + + def equivalentIsReflexive(p: Rational): Boolean = { + require(p.isRational) + p ~ p + } holds + + def equivalentIsSymmetric(p: Rational, q: Rational): Boolean = { + require(p.isRational && q.isRational && p ~ q) + q ~ p + } holds + + def equivalentIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = { + require(p.isRational && q.isRational && r.isRational && p ~ q && q ~ r) + p ~ r + } holds }