From 65268fe860a4195394ea7e9e950f7bc343a6601f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 16 Jul 2015 17:15:56 +0200
Subject: [PATCH] all properties of coins implemented

---
 testcases/proof/proba/Coins.scala | 114 +++++++++++++++---------------
 1 file changed, 57 insertions(+), 57 deletions(-)

diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala
index c85893820..1d2687a4a 100644
--- a/testcases/proof/proba/Coins.scala
+++ b/testcases/proof/proba/Coins.scala
@@ -119,12 +119,12 @@ object Coins {
   def sum(coin1: CoinDist, coin2: CoinDist): CoinDist = {
     require(isDist(coin1) && isDist(coin2))
     CoinDist(coin1.pHead*coin2.pHead + coin1.pTail*coin2.pTail)
-  } ensuring(res => res.pTail == (coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead))
+  } ensuring(res => isDist(res) && res.pTail == (coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead))
 
   def sum(dist: CoinsJoinDist): CoinDist = {
     require(isDist(dist))
     CoinDist(dist.hh + dist.tt)
-  } ensuring(res => res.pTail == (dist.ht + dist.th))
+  } ensuring(res => isDist(res) && res.pTail == (dist.ht + dist.th))
 
 
 
@@ -133,73 +133,73 @@ object Coins {
    *          properties of sum operation            *
    ***************************************************/
 
-  //def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
-  //  val dist = sum(coin1, coin2)
-  //  isUniform(dist)
-  //} holds
+  def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
+    val dist = sum(coin1, coin2)
+    isUniform(dist)
+  } holds
 
-  //def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
-  //  val dist = sum(coin1, coin2)
-  //  isUniform(dist)
-  //} holds
+  def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
+    val dist = sum(coin1, coin2)
+    isUniform(dist)
+  } holds
 
-  //def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
-  //  val dist = sum(sum(coin1, coin2), coin3)
-  //  isUniform(dist)
-  //} holds
+  def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
+    val dist = sum(sum(coin1, coin2), coin3)
+    isUniform(dist)
+  } holds
 
-  //def sumUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
-  //  require(isDist(dist) && isIndependent(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
-  //  val res = sum(dist)
-  //  isUniform(res)
-  //} holds
+  def sumUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+    require(isDist(dist) && isIndependent(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+    val res = sum(dist)
+    isUniform(res)
+  } holds
 
-  ////should find counterexample, indepenence is required
-  //def sumUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
-  //  require(isDist(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
-  //  val res = sum(dist)
-  //  isUniform(res)
-  //} holds
+  //should find counterexample, indepenence is required
+  def sumUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+    require(isDist(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+    val res = sum(dist)
+    isUniform(res)
+  } holds
 
 
   ////sum of two non-uniform dices is potentially uniform (no result)
-  //def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
-  //  val dist = sum(coin1, coin2)
-  //  !isUniform(dist)
-  //} holds
+  def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
+    val dist = sum(coin1, coin2)
+    !isUniform(dist)
+  } holds
 
-  //def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
-  //  val dist = sum(sum(coin1, coin2), coin3)
-  //  !isUniform(dist)
-  //} //holds
+  def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
+    val dist = sum(sum(coin1, coin2), coin3)
+    !isUniform(dist)
+  } holds
 
-  //def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
-  //  require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
-  //  val res = sum(dist)
-  //  !isUniform(res)
-  //} holds
+  def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+    require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+    val res = sum(dist)
+    !isUniform(res)
+  } holds
 
-  ////independence is required
-  //def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
-  //  require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
-  //  val res = sum(dist)
-  //  !isUniform(res)
-  //} holds
+  //independence is required
+  def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+    require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+    val res = sum(dist)
+    !isUniform(res)
+  } holds
 
 
-  //def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2))
-  //  sum(coin1, coin2) == sum(coin2, coin1)
-  //} holds
+  def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2))
+    sum(coin1, coin2) == sum(coin2, coin1)
+  } holds
 
-  //def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
-  //  require(isDist(coin1) && isDist(coin2) && isDist(coin3))
-  //  sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
-  //} //holds
+  def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3))
+    sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
+  } holds
 
 }
-- 
GitLab