diff --git a/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt b/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt new file mode 100644 index 0000000000000000000000000000000000000000..da29597252b6fc613f0d203ef67f564c85a0c33d --- /dev/null +++ b/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt @@ -0,0 +1,8 @@ +with postcondition: +update 0 0 ok 0.06 +updateElem 0 1 ok 0.03 +readOverWrite 0 0 ok 0.13 +without postcondition: +domain 0 1 ok 0.12 +find 0 1 ok < 0.01 +noDuplicates 0 1 ok < 0.01 diff --git a/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt b/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt new file mode 100644 index 0000000000000000000000000000000000000000..9001a41a27d8be3f60c9ac1924e9c7e979f90b7d --- /dev/null +++ b/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt @@ -0,0 +1,7 @@ +with postcondition: +size 0 0 ok 0.08 +sortedIns 1 0 ok 0.12 +buggySortedIns 1 0 ok 0.08 +sort 1 0 ok 0.08 +without postcondition: +isSorted 0 1 ok < 0.01 diff --git a/sas2011-testcases/eval-summary/ListOperations-evaluation.txt b/sas2011-testcases/eval-summary/ListOperations-evaluation.txt new file mode 100644 index 0000000000000000000000000000000000000000..38ce53439cbac7b225bc8fd98f90350810cdaff6 --- /dev/null +++ b/sas2011-testcases/eval-summary/ListOperations-evaluation.txt @@ -0,0 +1,19 @@ +with postcondition: +size 0 0 ok 0.13 +iplSize 0 0 ok < 0.01 +zip 1 1 ok 0.10 +sizeTailRecAcc 1 0 ok 0.02 +sizesAreEquiv 0 0 ok < 0.01 +sizeAndContent 0 0 ok < 0.01 +drunk 0 0 ok 0.04 +reverse 0 0 ok < 0.01 +reverse0 0 0 ok 0.05 +append 0 0 ok 0.04 +nilAppend 0 0 ok 0.05 +appendAssoc 0 0 ok 0.12 +revAuxBroken 0 0 err 0.06 +sizeAppend 0 0 ok 0.07 +concat 0 0 ok 0.05 +concat0 0 0 ok 0.15 +without postcondition: +sizeTailRec 1 0 ok < 0.01 diff --git a/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt b/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt new file mode 100644 index 0000000000000000000000000000000000000000..bc8081bd176ab93316aa2d9e1547b28107d1d061 --- /dev/null +++ b/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt @@ -0,0 +1,2 @@ +with postcondition: +wrongCommutative 0 0 err 0.44 diff --git a/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt b/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt new file mode 100644 index 0000000000000000000000000000000000000000..d182caa39f3c670cd34cbdb82fde05ee0ce59c12 --- /dev/null +++ b/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt @@ -0,0 +1,10 @@ +with postcondition: +simplify 0 0 ok 0.26 +nnf 0 1 ok 0.41 +simplifyBreaksNNF 0 0 err 0.53 +nnfIsStable 0 0 ok 0.25 +simplifyIsStable 0 0 ok 0.11 +without postcondition: +isNNF 0 1 ok < 0.01 +vars 6 1 ok 0.20 +fv 1 0 ok 0.04 diff --git a/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt b/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt new file mode 100644 index 0000000000000000000000000000000000000000..2009c372fff1254d1c6ac4586b2db1de54aedfd4 --- /dev/null +++ b/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt @@ -0,0 +1,10 @@ +with postcondition: +ins 2 0 ok 1.64 +makeBlack 0 0 ok 0.02 +add 2 0 ok 0.08 +buggyAdd 1 0 err 0.24 +balance 0 1 ok 0.11 +buggyBalance 0 1 err 0.03 +without postcondition: +redNodesHaveBlackChildren 0 1 ok 0.04 +blackHeight 0 1 ok < 0.01