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