summaryrefslogtreecommitdiff
path: root/Test/dafny4
ModeNameSize
-rw-r--r--ACL2-extractor.dfy6954logplain
-rw-r--r--ACL2-extractor.dfy.expect62logplain
-rw-r--r--BinarySearch.dfy2116logplain
-rw-r--r--BinarySearch.dfy.expect337logplain
-rw-r--r--Bug54.dfy426logplain
-rw-r--r--Bug54.dfy.expect61logplain
-rw-r--r--Bug55.dfy253logplain
-rw-r--r--Bug55.dfy.expect61logplain
-rw-r--r--Bug56.dfy555logplain
-rw-r--r--Bug56.dfy.expect61logplain
-rw-r--r--Bug58.dfy386logplain
-rw-r--r--Bug58.dfy.expect61logplain
-rw-r--r--Bug60.dfy357logplain
-rw-r--r--Bug60.dfy.expect157logplain
-rw-r--r--Bug62.dfy547logplain
-rw-r--r--Bug62.dfy.expect61logplain
-rw-r--r--Bug63.dfy207logplain
-rw-r--r--Bug63.dfy.expect61logplain
-rw-r--r--Bug67.dfy278logplain
-rw-r--r--Bug67.dfy.expect115logplain
-rw-r--r--Bug68.dfy1432logplain
-rw-r--r--Bug68.dfy.expect142logplain
-rw-r--r--Bug69.dfy307logplain
-rw-r--r--Bug69.dfy.expect61logplain
-rw-r--r--Bug70.dfy280logplain
-rw-r--r--Bug70.dfy.expect61logplain
-rw-r--r--Bug71.dfy280logplain
-rw-r--r--Bug71.dfy.expect61logplain
-rw-r--r--Bug72.dfy464logplain
-rw-r--r--Bug73.dfy274logplain
-rw-r--r--Bug73.dfy.expect327logplain
-rw-r--r--Circ.dfy2270logplain
-rw-r--r--Circ.dfy.expect62logplain
-rw-r--r--ClassRefinement.dfy1578logplain
-rw-r--r--ClassRefinement.dfy.expect62logplain
-rw-r--r--CoqArt-InsertionSort.dfy4324logplain
-rw-r--r--CoqArt-InsertionSort.dfy.expect62logplain
-rw-r--r--Fstar-QuickSort.dfy4379logplain
-rw-r--r--Fstar-QuickSort.dfy.expect61logplain
-rw-r--r--GHC-MergeSort.dfy22351logplain
-rw-r--r--GHC-MergeSort.dfy.expect62logplain
-rw-r--r--Juggernaut.dfy335logplain
-rw-r--r--Juggernaut.dfy.expect61logplain
-rw-r--r--KozenSilva.dfy13509logplain
-rw-r--r--KozenSilva.dfy.expect62logplain
-rw-r--r--NipkowKlein-chapter3.dfy8619logplain
-rw-r--r--NipkowKlein-chapter3.dfy.expect62logplain
-rw-r--r--NipkowKlein-chapter7.dfy15863logplain
-rw-r--r--NipkowKlein-chapter7.dfy.expect62logplain
-rw-r--r--NumberRepresentations.dfy9551logplain
-rw-r--r--NumberRepresentations.dfy.expect62logplain
-rw-r--r--Primes.dfy5470logplain
-rw-r--r--Primes.dfy.expect62logplain
-rw-r--r--SoftwareFoundations-Basics.dfy11485logplain
-rw-r--r--SoftwareFoundations-Basics.dfy.expect164logplain
-rw-r--r--bug72.dfy.expect61logplain
-rw-r--r--set-compr.dfy1604logplain
-rw-r--r--set-compr.dfy.expect379logplain