Regular Language Typing Experiments

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.

First order

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

Higher order

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