summaryrefslogtreecommitdiff
path: root/Test/dafny0
ModeNameSize
-rw-r--r--AdvancedLHS.dfy1541logplain
-rw-r--r--AdvancedLHS.dfy.expect178logplain
-rw-r--r--Array.dfy8343logplain
-rw-r--r--Array.dfy.expect3710logplain
-rw-r--r--AssumptionVariables0.dfy1225logplain
-rw-r--r--AssumptionVariables0.dfy.expect1956logplain
-rw-r--r--AssumptionVariables1.dfy585logplain
-rw-r--r--AssumptionVariables1.dfy.expect61logplain
-rw-r--r--AutoReq.dfy5625logplain
-rw-r--r--AutoReq.dfy.expect1448logplain
-rw-r--r--BadFunction.dfy487logplain
-rw-r--r--BadFunction.dfy.expect189logplain
-rw-r--r--Basics.dfy13001logplain
-rw-r--r--Basics.dfy.expect2316logplain
-rw-r--r--Calculations.dfy2382logplain
-rw-r--r--Calculations.dfy.expect811logplain
-rw-r--r--CallStmtTests.dfy429logplain
-rw-r--r--CallStmtTests.dfy.expect228logplain
-rw-r--r--ChainingDisjointTests.dfy1013logplain
-rw-r--r--ChainingDisjointTests.dfy.expect61logplain
-rw-r--r--CoPrefix.dfy4413logplain
-rw-r--r--CoPrefix.dfy.expect1860logplain
-rw-r--r--CoResolution.dfy4485logplain
-rw-r--r--CoResolution.dfy.expect2482logplain
-rw-r--r--Coinductive.dfy5196logplain
-rw-r--r--Coinductive.dfy.expect2320logplain
-rw-r--r--CoinductiveProofs.dfy4329logplain
-rw-r--r--CoinductiveProofs.dfy.expect2122logplain
-rw-r--r--Compilation.dfy4066logplain
-rw-r--r--Compilation.dfy.expect102logplain
-rw-r--r--CompilationErrors.dfy864logplain
-rw-r--r--CompilationErrors.dfy.expect767logplain
-rw-r--r--Comprehensions.dfy1379logplain
-rw-r--r--Comprehensions.dfy.expect282logplain
-rw-r--r--Computations.dfy5225logplain
-rw-r--r--Computations.dfy.expect62logplain
-rw-r--r--ComputationsLoop.dfy252logplain
-rw-r--r--ComputationsLoop.dfy.expect288logplain
-rw-r--r--ComputationsLoop2.dfy303logplain
-rw-r--r--ComputationsLoop2.dfy.expect464logplain
-rw-r--r--ComputationsNeg.dfy1050logplain
-rw-r--r--ComputationsNeg.dfy.expect826logplain
-rw-r--r--ControlStructures.dfy6502logplain
-rw-r--r--ControlStructures.dfy.expect4210logplain
-rw-r--r--Corecursion.dfy5573logplain
-rw-r--r--Corecursion.dfy.expect1901logplain
-rw-r--r--DTypes.dfy5124logplain
-rw-r--r--DTypes.dfy.expect984logplain
-rw-r--r--DatatypeUpdate.dfy972logplain
-rw-r--r--DatatypeUpdate.dfy.expect61logplain
-rw-r--r--Datatypes.dfy7960logplain
-rw-r--r--Datatypes.dfy.expect2233logplain
-rw-r--r--Definedness.dfy6389logplain
-rw-r--r--Definedness.dfy.expect6401logplain
-rw-r--r--DirtyLoops.dfy214logplain
-rw-r--r--DirtyLoops.dfy.expect122logplain
-rw-r--r--DisplayExpressions.dfy224logplain
-rw-r--r--DisplayExpressions.dfy.expect577logplain
-rw-r--r--EqualityTypes.dfy7420logplain
-rw-r--r--EqualityTypes.dfy.expect3950logplain
-rw-r--r--FunctionSpecifications.dfy4574logplain
-rw-r--r--FunctionSpecifications.dfy.expect2804logplain
-rw-r--r--Include.dfy793logplain
-rw-r--r--Include.dfy.expect631logplain
-rw-r--r--Includee.dfy563logplain
-rw-r--r--Includee.dfy.expect564logplain
-rw-r--r--Inverses.dfy4133logplain
-rw-r--r--Inverses.dfy.expect528logplain
-rw-r--r--IteratorResolution.dfy3631logplain
-rw-r--r--IteratorResolution.dfy.expect1141logplain
-rw-r--r--Iterators.dfy9056logplain
-rw-r--r--Iterators.dfy.expect3379logplain
-rw-r--r--LetExpr.dfy7918logplain
-rw-r--r--LetExpr.dfy.expect1095logplain
-rw-r--r--LiberalEquality.dfy1026logplain
-rw-r--r--LiberalEquality.dfy.expect356logplain
-rw-r--r--LoopModifies.dfy6905logplain
-rw-r--r--LoopModifies.dfy.expect2823logplain
-rw-r--r--Maps.dfy4187logplain
-rw-r--r--Maps.dfy.expect233logplain
-rw-r--r--MatchBraces.dfy3035logplain
-rw-r--r--MatchBraces.dfy.expect2617logplain
-rw-r--r--ModifyStmt.dfy3941logplain
-rw-r--r--ModifyStmt.dfy.expect1382logplain
-rw-r--r--Modules0.dfy7566logplain
-rw-r--r--Modules0.dfy.expect3652logplain
-rw-r--r--Modules1.dfy2449logplain
-rw-r--r--Modules1.dfy.expect602logplain
-rw-r--r--Modules2.dfy1661logplain
-rw-r--r--Modules2.dfy.expect634logplain
-rw-r--r--ModulesCycle.dfy265logplain
-rw-r--r--ModulesCycle.dfy.expect249logplain
-rw-r--r--MultiDimArray.dfy2384logplain
-rw-r--r--MultiDimArray.dfy.expect335logplain
-rw-r--r--MultiSets.dfy8136logplain
-rw-r--r--MultiSets.dfy.expect970logplain
-rw-r--r--NatTypes.dfy2922logplain
-rw-r--r--NatTypes.dfy.expect1313logplain
-rw-r--r--NoTypeArgs.dfy2097logplain
-rw-r--r--NoTypeArgs.dfy.expect62logplain
-rw-r--r--NonGhostQuantifiers.dfy7074logplain
-rw-r--r--NonGhostQuantifiers.dfy.expect3969logplain
-rw-r--r--OpaqueFunctions.dfy4228logplain
-rw-r--r--OpaqueFunctions.dfy.expect2869logplain
-rw-r--r--OpaqueFunctionsFail.dfy311logplain
-rw-r--r--OpaqueFunctionsFail.dfy.expect561logplain
-rw-r--r--Parallel.dfy8018logplain
-rw-r--r--Parallel.dfy.expect2005logplain
-rw-r--r--ParallelResolveErrors.dfy3676logplain
-rw-r--r--ParallelResolveErrors.dfy.expect2702logplain
-rw-r--r--ParseErrors.dfy2031logplain
-rw-r--r--ParseErrors.dfy.expect1177logplain
-rw-r--r--PredExpr.dfy1896logplain
-rw-r--r--PredExpr.dfy.expect592logplain
-rw-r--r--Predicates.dfy3551logplain
-rw-r--r--Predicates.dfy.expect1273logplain
-rw-r--r--RankNeg.dfy746logplain
-rw-r--r--RankNeg.dfy.expect737logplain
-rw-r--r--RankPos.dfy1618logplain
-rw-r--r--RankPos.dfy.expect62logplain
-rw-r--r--Reads.dfy1126logplain
-rw-r--r--Reads.dfy.expect774logplain
-rw-r--r--RealCompare.dfy2350logplain
-rw-r--r--RealCompare.dfy.expect757logplain
-rw-r--r--RealTypes.dfy899logplain
-rw-r--r--RealTypes.dfy.expect522logplain
-rw-r--r--Refinement.dfy3891logplain
-rw-r--r--Refinement.dfy.expect1860logplain
-rw-r--r--RefinementErrors.dfy1687logplain
-rw-r--r--RefinementErrors.dfy.expect1614logplain
-rw-r--r--RefinementModificationChecking.dfy548logplain
-rw-r--r--RefinementModificationChecking.dfy.expect263logplain
-rw-r--r--ResolutionErrors.dfy30150logplain
-rw-r--r--ResolutionErrors.dfy.expect18124logplain
-rw-r--r--ReturnErrors.dfy843logplain
-rw-r--r--ReturnErrors.dfy.expect324logplain
-rw-r--r--ReturnTests.dfy1493logplain
-rw-r--r--ReturnTests.dfy.expect62logplain
-rw-r--r--SeqSlice.dfy889logplain
-rw-r--r--SeqSlice.dfy.expect61logplain
-rw-r--r--Simple.dfy1433logplain
-rw-r--r--Simple.dfy.expect1356logplain
-rw-r--r--Skeletons.dfy1051logplain
-rw-r--r--Skeletons.dfy.expect474logplain
-rw-r--r--SmallTests.dfy18262logplain
-rw-r--r--SmallTests.dfy.expect6187logplain
-rw-r--r--SplitExpr.dfy3036logplain
-rw-r--r--SplitExpr.dfy.expect215logplain
-rw-r--r--StatementExpressions.dfy2692logplain
-rw-r--r--StatementExpressions.dfy.expect840logplain
-rw-r--r--Superposition.dfy1566logplain
-rw-r--r--Superposition.dfy.expect1596logplain
-rw-r--r--TailCalls.dfy3023logplain
-rw-r--r--TailCalls.dfy.expect530logplain
-rw-r--r--Termination.dfy9257logplain
-rw-r--r--Termination.dfy.expect1967logplain
d---------Trait816logplain
-rw-r--r--Tuples.dfy800logplain
-rw-r--r--Tuples.dfy.expect233logplain
-rw-r--r--TypeAntecedents.dfy2748logplain
-rw-r--r--TypeAntecedents.dfy.expect784logplain
-rw-r--r--TypeInstantiations.dfy1630logplain
-rw-r--r--TypeInstantiations.dfy.expect1822logplain
-rw-r--r--TypeParameters.dfy7022logplain
-rw-r--r--TypeParameters.dfy.expect1756logplain
-rw-r--r--TypeSynonyms.dfy972logplain
-rw-r--r--TypeSynonyms.dfy.expect61logplain
-rw-r--r--TypeTests.dfy4639logplain
-rw-r--r--TypeTests.dfy.expect2985logplain
d---------snapshots856logplain