The following tables summarizes the result of our verification technique on several test files. Each row correspond to one test file and has the following format:
| Specification file link | Verified property | ✘ | P/C | Time | Trace |
The result of the experiment is given by the P/C column, where we note P when the property is successuly proved, or C when a counter example is found (the property is successuly disproved). The complete output of the verification program is given by the trace file (a description of a typical trace can be found here). It includes the final abstraction used to prove/disprove the property as a tree automaton, and a list of all the different ways to type the input pattern. For some experiments we judged necessary to disable the constants subtyping phase to obtain better performances. This is indicated by the presence of a ✘ symbol.
A detailed description of the specification file format is given here. Experiments were performed on an Intel® i7-7600U CPU, 4 2.80GHz cores with a timeout time of 120s.
| Timbuk specifications | |||||
|---|---|---|---|---|---|
| insertionSort | sorted(insertionSort A_and_B_list) | P | 0.627 | trace | |
| orderedTreeTraversal | sorted (infix-traversal ordered_A_and_B_tree) | P | 4.72 | trace | |
| deleteImplies | (member Y AnyList) ∧ (not (eq X Y)) → member Y (delete X AnyList) | P | 0.7 | trace | |
| reverseImplies | (sorted L) → (invsorted (reverse L)) | P | 1.402 | trace | |
| replaceTree | not (member A (replace A C A_and_B_tree)) | P | 0.751 | trace | |
| reverse | invsorted (reverse [A,…A,B,…,B]) | P | 2.352 | trace | |
| insertTree | ordered (insert A_and_B_list emptyTree) | - | Timeout | ||
| split | let (l1,l2) = split [A,B,A,B,…] in not(member B l1) ∧ (member A l2) | P | 0.688 | trace | |
| orderedTree | (ordered ordered_A_and_B_tree) | ✘ | P | 7.097 | trace |
| delete | member X (delete X AnyList) is false | P | 0.369 | trace | |
| deleteBUG | (member X (deleteBUG X AnyList)) is false | C | 0.32 | trace | |
| reverseBUGimplies | (member X L) → (member X (reverseBUG L)) | C | 0.417 | trace | |
| orderedTreeTraversalBug | sorted (prefix-traversal ordered_A_and_B_tree) | C | 47.847 | trace | |
| MoCHi specifications | |||||
|---|---|---|---|---|---|
| makelist | let L= makelist(X,Y) in null(L) ∨ member(Y,L) | P | 0.49 | trace | |
| headReverse | X>0 → hd(reverse(makelist X)) > 0 | P | 1.258 | trace | |
| zipUnzip | let l1,l2 = unzip (makelist_of_pairs N) in zip l1 l2 does not throw an exception | - | Timeout | ||
| treeDepth | (depth(X)≥0 ∧ depth(Y)≥0) → depth(Node(_,X,Y))>0 | P | 0.919 | trace | |
| Own specifications | |||||
|---|---|---|---|---|---|
| incTree | !member(0, inc(T)) | P | 0.423 | trace | |
| if | Typing if-the-else | C | 0.023 | trace | |
| sorted | all possible regular typings for (sorted L) | C | 0.229 | trace | |
| appendTheorem | eql((append L1 L2),nil) ↔ (eql(L1,nil) ∧ eql(L2,nil)) | P | 0.321 | trace | |
| iteEvenOdd | if even(X) then odd(s(X)) else odd(X) | P | 0.181 | trace | |
| even | all possible regular typings for (even X) | P | 0.111 | trace | |
| reverseReverseImplies | (sorted L) → (sorted (reverse (reverse L))) | P | 2.312 | trace | |
| evenOdd | Y > 0 => (even(X) ≤> even(power(X,Y))) | P | 0.399 | trace | |
| insertionSort2 | member(X,L) ↔ member(X,(insertionSort L)) | P | 0.818 | trace | |
| mergeSort | sorted(mergeSort A_and_B_list) | ✘ | P | 1.525 | trace |
| mult | (mult X 0) = 0 | P | 0.134 | trace | |
| deleteTyping | all possible regular typings for (deleteBug X L) | P | 0.215 | trace | |
| equalNat | X = Y => X = X | - | Timeout | ||
| mergeSort2 | member(X,L) ↔ member(X,(mergeSortBug L)) | ✘ | - | Timeout | |
| plusEven | even(plus(X,X)) | P | 0.167 | trace | |
| memberTree | (member X T) ↔ (member X (mirror T)) | P | 4.25 | trace | |
| heightTree | ((height T)=2) ↔ (height (mirror T) =2) | - | Timeout | ||
| equal | - | Timeout | |||
| all-a | allA([cons(A, *|nil)]) = true | P | 0.058 | trace | |
| memberAppend | (member X (append L1 L2)) ↔ ((member X L1) ∨ (member X L2)) | P | 0.506 | trace | |
| square | (square X) != 2 | P | 0.553 | trace | |
| orderedTreePredicate | all possible regular typings for (ordered T) | P | 44.348 | trace | |
| equalLength | length (minAndMax nat_list) = 2 | P | 1.626 | trace | |
| plusEvenError | even(plus(X,Y)) | C | 0.169 | trace | |
| orderedTreePredicate2 | (ordered T)::true | C | 40.792 | trace | |
| memberAppendError | (member X (append L1 L2)) ↔ ((member X L1) ∧ (member X L2)) | C | 0.504 | trace | |
| insertionSort2BUG | member(X, L) <-> member(X, insertionSort(L)) is false | C | 0.816 | trace | |
| simple | Non-deterministic f(X) != false | C | 0.049 | trace | |
| appendTheoremBug | eql((appendB L1 L2),nil) ↔ (eql(L1,nil) ∧ eql(L2,nil)) | C | 0.354 | trace | |
| Timbuk specifications | |||||
|---|---|---|---|---|---|
| foldRightMult | (foldRight mult nonzero_nat_list 1) is not 0 | - | issue #1 | ||
| mapSquare | (filter (eq 2) (map square nat_list)) is empty | - | Timeout | ||
| insertionSortHO | (sorted leq (insertionSort leq A_and_B_list)) | - | issue #2 | trace | |
| foldLeftPlus | even (foldLeft plus 0 even_nat_list) | - | issue #2 | trace | |
| mapPlus | no 0 in (map (plus 1) nat_list) | P | 0.416 | trace | |
| filterNz | (forAll nz (filter nz nat_list)) | P | 0.423 | trace | |
| mapTree | not (member 0 (map (plus 1) nat_tree) | P | 0.561 | trace | |
| filterEven | forall even (filter even nat_list) | P | 0.462 | trace | |
| filterEvenBug | exists odd (filter even nat_list) | C | 0.542 | trace | |
| insertionSortHObug | sorted (≥) (sort (≤) A_and_B_list) | - | issue #3 | trace | |
| MoCHi specifications | |||||
|---|---|---|---|---|---|
| mapFilter | map head (filter nonEmpty nat_list) does not throw an exception | P | 0.906 | trace | |
| foldDiv | foldLeft div X (makelist Y) does not throw an exception | P | 0.244 | trace | |
| forallLeq | forall (leq 1) (makelist X) | P | 0.4 | trace | |
| Own specifications | |||||
|---|---|---|---|---|---|
| exists | all possible regular typings for (exists (eq X) A_and_B_list) | P | 0.275 | trace | |
| exprSimplif | - | Timeout | |||
| forallNotEquivalentNotExists | (forall (neq A) L) ↔ (not(exists (eq A) L)) | P | 0.541 | trace | |
| forallImpliesExists | (not(null(L)) ∧ (forall (eq A) L)) → (exists (eq A) L) | P | 0.53 | trace | |
| exists2 | all possible regular typings for (exists P A_and_B_list) | P | 0.413 | trace | |
| forall | all possible regular typings for (forall (eq X) A_and_B_list) | P | 0.239 | trace | |
| map2AddImplies | !member(0, L1) ∧ !member(0, L2) → !member(0, map2 add L1 L2) | - | Timeout | ||
| leq | - | Timeout | |||
| mergeSortHO | sorted leq (mergeSort leq A_and_B_list) | ✘ | P | 1.67 | trace |
| filterEquivExists | (exists (eq A) L) ↔ (not(null(filter (eq A) L)) | P | 0.816 | trace | |
| mergeSortHObug | (sorted geq (mergeSort leq A_and_B_list)) | - | Timeout | ||
| forallNotEquivalentNotForall | (forall (neq A) L) ↔ (not(forall (eq A) L)) | C | 0.509 | trace | |
| forallImpliesExistsError | (forall (eq A) L) → (exists (eq A) L) | C | 0.462 | trace | |