## AssociativityProperties.scala [raw]

```import stainless.lang._

object AssociativityProperties {

def isAssociative[A](f: (A,A) => A): Boolean = {
forall((x: A, y: A, z: A) => f(f(x, y), z) == f(x, f(y, z)))
}

def isCommutative[A](f: (A,A) => A): Boolean = {
forall((x: A, y: A) => f(x, y) == f(y, x))
}

def isRotate[A](f: (A,A) => A): Boolean = {
forall((x: A, y: A, z: A) => f(f(x, y), z) == f(f(y, z), x))
}

def assocNotCommutative[A](f: (A,A) => A): Boolean = {
require(isAssociative(f))
isCommutative(f)
}.holds
// Counterexample for postcondition violation in `assocNotCommutative`:
//   when f is:
//     (x\$412: A, x\$413: A) => if (x\$412 == A#3 && x\$413 == A#3) {
//       A#3
//     } else if (x\$412 == A#3 && x\$413 == A#2) {
//       A#3
//     } else if (x\$412 == A#2 && x\$413 == A#3) {
//       A#2
//     } else if (x\$412 == A#2 && x\$413 == A#2) {
//       A#2
//     } else if (x\$412 == A#3) {
//       A#3
//     } else if (x\$413 == A#2) {
//       A#2
//     } else if (x\$412 == A#2) {
//       A#2
//     } else if (x\$413 == A#3) {
//       A#2
//     } else if (true) {
//       A#2
//     } else {
//       A#2
//     }

def commNotAssociative[A](f: (A,A) => A): Boolean = {
require(isCommutative(f))
isAssociative(f)
}.holds
// Counterexample for postcondition violation in `commNotAssociative`:
//   when f is:
//     (x\$330: A, x\$331: A) => if (x\$330 == A#2 && x\$331 == A#0) {
//       A#2
//     } else if (x\$330 == A#0 && x\$331 == A#0) {
//       A#1
//     } else if (x\$330 == A#2 && x\$331 == A#2) {
//       A#0
//     } else if (x\$330 == A#0 && x\$331 == A#2) {
//       A#2
//     } else if (x\$331 == A#0) {
//       A#2
//     } else if (x\$331 == A#2) {
//       A#0
//     } else if (x\$330 == A#2) {
//       A#0
//     } else if (x\$330 == A#0) {
//       A#2
//     } else if (true) {
//       A#0
//     } else {
//       A#0
//     }
}
```

back