diff options
51 files changed, 6694 insertions, 11 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e72c04dd..fa8ea6da 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -42,6 +42,7 @@ namespace Microsoft.Dafny { string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))
{
+ IncludeCodeContracts();
while (true) {
string s = rd.ReadLine();
if (s == null)
@@ -415,7 +416,7 @@ namespace Microsoft.Dafny { }
}
wr.Write(")");
-
+
wr.WriteLine(";");
Indent(ind + 2 * IndentAmount);
wr.WriteLine("}");
@@ -573,6 +574,8 @@ namespace Microsoft.Dafny { WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
wr.WriteLine(")");
Indent(indent); wr.WriteLine("{");
+ TrReq(m.Req, indent + IndentAmount);
+ TrEns(m.Ens, indent + IndentAmount);
foreach (Formal p in m.Outs) {
if (!p.IsGhost) {
Indent(indent + IndentAmount);
@@ -852,12 +855,20 @@ namespace Microsoft.Dafny { void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
- if (stmt.IsGhost) {
+ if (!DafnyOptions.O.RuntimeChecking && stmt.IsGhost) {
CheckHasNoAssumes(stmt);
return;
}
- if (stmt is PrintStmt) {
+ if (stmt is AssumeStmt)
+ {
+ TrAssumeStmt((AssumeStmt)stmt, indent);
+ }
+ else if (stmt is AssertStmt)
+ {
+ TrAssertStmt((AssertStmt)stmt, indent);
+ }
+ else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (Attributes.Argument arg in s.Args) {
SpillLetVariableDecls(arg.E, indent);
@@ -2210,5 +2221,107 @@ namespace Microsoft.Dafny { }
twr.Write(")");
}
+
+ #region Runtime checking translation
+
+ void IncludeCodeContracts()
+ {
+ if (DafnyOptions.O.RuntimeChecking)
+ {
+ wr.WriteLine("using System.Diagnostics.Contracts;");
+ }
+ }
+
+ void TrAssumeStmt(AssumeStmt/*!*/ stmt, int indent)
+ {
+ Contract.Requires(stmt != null);
+
+ Contract.Assert(DafnyOptions.O.RuntimeChecking);
+ WriteAssumption(ExprToString(stmt.Expr), indent);
+ }
+
+ void TrAssertStmt(AssertStmt/*!*/ stmt, int indent)
+ {
+ Contract.Requires(stmt != null);
+
+ Contract.Assert(DafnyOptions.O.RuntimeChecking);
+ WriteAssertion(ExprToString(stmt.Expr), indent);
+ }
+
+ void TrReq(List<MaybeFreeExpression/*!*/>/*!*/ req, int indent)
+ {
+ Contract.Requires(cce.NonNullElements(req));
+
+ if (DafnyOptions.O.RuntimeChecking)
+ {
+ foreach (MaybeFreeExpression e in req)
+ {
+ if (!e.IsFree)
+ {
+ Indent(indent);
+ wr.Write("Contract.Requires(");
+ TrExpr(e.E);
+ wr.WriteLine(");");
+ }
+ }
+ }
+ }
+
+ void TrEns(List<MaybeFreeExpression/*!*/>/*!*/ ens, int indent)
+ {
+ Contract.Requires(cce.NonNullElements(ens));
+
+ if (DafnyOptions.O.RuntimeChecking)
+ {
+ foreach (MaybeFreeExpression e in ens)
+ {
+ if (!e.IsFree)
+ {
+ Indent(indent);
+ wr.Write("Contract.Ensures(");
+ TrExpr(e.E);
+ wr.WriteLine(");");
+ }
+ }
+ }
+ }
+
+ #endregion
+
+ #region Runtime checking helper methods
+
+ string/*!*/ ExprToString(Expression/*!*/ expr)
+ {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ TextWriter oldWr = wr;
+ wr = new StringWriter();
+ TrExpr(expr);
+ string e = wr.ToString();
+ wr = oldWr;
+ return e;
+ }
+
+ void WriteAssumption(string/*!*/ expr, int indent)
+ {
+ Contract.Requires(expr != null);
+
+ Contract.Assert(DafnyOptions.O.RuntimeChecking);
+ Indent(indent);
+ wr.WriteLine("Contract.Assume(" + expr + ");");
+ }
+
+ void WriteAssertion(string/*!*/ expr, int indent)
+ {
+ Contract.Requires(expr != null);
+
+ Contract.Assert(DafnyOptions.O.RuntimeChecking);
+ Indent(indent);
+ wr.WriteLine("Contract.Assert(" + expr + ");");
+ }
+
+ #endregion
+
}
}
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 34fa0487..cb126446 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -33,6 +33,8 @@ namespace Microsoft.Dafny public bool Compile = true;
public bool ForceCompile = false;
public bool SpillTargetCode = false;
+ public bool Verification = true;
+ public bool RuntimeChecking = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -90,6 +92,22 @@ namespace Microsoft.Dafny ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
+ case "verification":
+ int verification = 1; // 1 is default, verification
+ if (ps.GetNumericArgument(ref verification, 2))
+ {
+ Verification = verification == 1;
+ }
+ return true;
+
+ case "runtimeChecking":
+ int runtimeChecking = 0; // 0 is default, no runtime checking
+ if (ps.GetNumericArgument(ref runtimeChecking, 2))
+ {
+ RuntimeChecking = runtimeChecking == 1;
+ }
+ return true;
+
default:
break;
}
@@ -148,6 +166,13 @@ namespace Microsoft.Dafny 1,2,3,4,5 - levels in between, ordered as follows as far as
how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
6 (default) - most discriminating
+ /verification:<n>
+ 0 - do not verify the Dafny program
+ 1 (default) - verify the Dafny program
+ /runtimeChecking:<n>
+ 0 (default) - ignore Dafny specifications during compilation
+ 1 - translate Dafny specifications to CodeContracts during
+ compilation for runtime checking
");
base.Usage(); // also print the Boogie options
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 3534dcbf..2f7175f4 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -23,6 +23,7 @@ namespace Microsoft.Dafny using VC;
using System.CodeDom.Compiler;
using AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Win32; // needed for ccrewrite
public class DafnyDriver
{
@@ -150,7 +151,7 @@ namespace Microsoft.Dafny if (err != null) {
exitValue = ExitValue.DAFNY_ERROR;
ErrorWriteLine(err);
- } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck && DafnyOptions.O.Verification) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
@@ -187,6 +188,14 @@ namespace Microsoft.Dafny }
exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED;
}
+ else if (!DafnyOptions.O.Verification)
+ {
+ if (DafnyOptions.O.ForceCompile)
+ {
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
+ }
+ exitValue = ExitValue.NOT_VERIFIED;
+ }
}
return exitValue;
}
@@ -231,10 +240,33 @@ namespace Microsoft.Dafny }
cp.GenerateInMemory = false;
cp.ReferencedAssemblies.Add("System.Numerics.dll");
+ string ccrewriter = findCCRewriter();
+ bool ccrewrite = DafnyOptions.O.RuntimeChecking && ccrewriter != null;
+ if (ccrewrite)
+ {
+ cp.CompilerOptions += " /D:CONTRACTS_FULL";
+ }
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
if (cr.Errors.Count == 0) {
Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
+ if (ccrewrite)
+ {
+ Process p = new Process();
+ string ccrewriterOpts = "-nologo -callSiteRequires -shortBranches -throwOnFailure";
+ p.StartInfo.FileName = "cmd.exe";
+ p.StartInfo.Arguments = "/C \"\"" + ccrewriter + "\" " +
+ ccrewriterOpts + " \"" + cp.OutputAssembly + "\"\"";
+ p.StartInfo.UseShellExecute = false;
+ p.StartInfo.RedirectStandardOutput = true;
+ p.Start();
+ p.WaitForExit();
+ Console.WriteLine("Rewrote assembly into {0}", cr.PathToAssembly);
+ }
+ else if (ccrewriter == null)
+ {
+ Console.WriteLine("Error: cannot rewrite, because there is no CodeContracts rewriter");
+ }
} else {
Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
foreach (var ce in cr.Errors) {
@@ -787,5 +819,56 @@ namespace Microsoft.Dafny return PipelineOutcome.VerificationCompleted;
}
+
+ #region Runtime checking
+
+ /********** Find Code Contracts rewriter **********/
+ private static string findCCRewriter()
+ {
+ using (RegistryKey rk = Registry.CurrentUser.OpenSubKey(@"SOFTWARE"))
+ {
+ foreach (string skN0 in rk.GetSubKeyNames())
+ if (skN0 == "Microsoft")
+ using (RegistryKey sk0 = rk.OpenSubKey(skN0))
+ {
+ foreach (string skN1 in sk0.GetSubKeyNames())
+ if (skN1 == "VisualStudio")
+ using (RegistryKey sk1 = sk0.OpenSubKey(skN1))
+ {
+ foreach (string skN2 in sk1.GetSubKeyNames())
+ using (RegistryKey sk2 = sk1.OpenSubKey(skN2))
+ {
+ foreach (string skN3 in sk2.GetSubKeyNames())
+ if (skN3 == "CodeTools")
+ using (RegistryKey sk3 = sk2.OpenSubKey(skN3))
+ {
+ foreach (string skN4 in sk3.GetSubKeyNames())
+ if (skN4 == "CodeContracts")
+ using (RegistryKey sk4 = sk3.OpenSubKey(skN4))
+ {
+ if ((string)sk4.GetValue("DisplayName") ==
+ "Microsoft Code Contracts")
+ {
+ string ccrewriter =
+ (string)sk4.GetValue("InstallDir") +
+ "Bin\\ccrewrite.exe";
+ if (File.Exists(ccrewriter))
+ return ccrewriter;
+ else
+ return null;
+ }
+ else
+ return null;
+ }
+ }
+ }
+ }
+ }
+ return null;
+ }
+ }
+
+ #endregion
+
}
}
diff --git a/Test/VSComp2010/AnswerNoRuntimeChecking b/Test/VSComp2010/AnswerNoRuntimeChecking new file mode 100644 index 00000000..d0492caf --- /dev/null +++ b/Test/VSComp2010/AnswerNoRuntimeChecking @@ -0,0 +1,15 @@ +
+-------------------- Problem1-SumMax --------------------
+Compiled assembly into Problem1-SumMax.exe
+
+-------------------- Problem2-Invert --------------------
+Compiled assembly into Problem2-Invert.exe
+
+-------------------- Problem3-FindZero --------------------
+Compiled assembly into Problem3-FindZero.exe
+
+-------------------- Problem4-Queens --------------------
+Compiled assembly into Problem4-Queens.exe
+
+-------------------- Problem5-DoubleEndedQueue --------------------
+Compiled assembly into Problem5-DoubleEndedQueue.dll
diff --git a/Test/VSComp2010/AnswerRuntimeChecking b/Test/VSComp2010/AnswerRuntimeChecking new file mode 100644 index 00000000..858b6370 --- /dev/null +++ b/Test/VSComp2010/AnswerRuntimeChecking @@ -0,0 +1,4 @@ +
+-------------------- Problem1-SumMax --------------------
+Compiled assembly into Problem1-SumMax.exe
+Rewrote assembly into Problem1-SumMax.exe
diff --git a/Test/VSComp2010/runtestNoRuntimeChecking.bat b/Test/VSComp2010/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..4efd244a --- /dev/null +++ b/Test/VSComp2010/runtestNoRuntimeChecking.bat @@ -0,0 +1,28 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (Problem1-SumMax Problem2-Invert Problem3-FindZero
+ Problem4-Queens Problem5-DoubleEndedQueue) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/VSComp2010/runtestRuntimeChecking.bat b/Test/VSComp2010/runtestRuntimeChecking.bat new file mode 100644 index 00000000..d3b8a733 --- /dev/null +++ b/Test/VSComp2010/runtestRuntimeChecking.bat @@ -0,0 +1,33 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM Problem2-Invert : quantifiers
+REM Problem3-FindZero : ghost state
+REM Problem4-Queens : quantifiers
+REM Problem5-DoubleEndedQueue: ghost state
+
+for %%f in (Problem1-SumMax) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking new file mode 100644 index 00000000..81ac67ef --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking @@ -0,0 +1,32 @@ +
+-------------------- b1 --------------------
+Compiled assembly into b1.exe
+
+-------------------- b2 --------------------
+Compiled assembly into b2.exe
+
+-------------------- b3 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b4 --------------------
+Compiled assembly into b4.dll
+
+-------------------- b5 --------------------
+Compiled assembly into b5.dll
+
+-------------------- b6 --------------------
+Compiled assembly into b6.exe
+
+-------------------- b7 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking new file mode 100644 index 00000000..49a440db --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking @@ -0,0 +1,21 @@ +
+-------------------- b1 --------------------
+Compiled assembly into b1.exe
+Rewrote assembly into b1.exe
+
+-------------------- b3 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b7 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..c85b7606 --- /dev/null +++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat @@ -0,0 +1,27 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (b1 b2 b3 b4 b5 b6 b7 b8) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat new file mode 100644 index 00000000..27df70a3 --- /dev/null +++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat @@ -0,0 +1,33 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM b2: quantifiers
+REM b4: old expressions
+REM b5: parallel statements
+REM b6: functions
+
+for %%f in (b1 b3 b7 b8) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny0/AnswerNoRuntimeChecking b/Test/dafny0/AnswerNoRuntimeChecking new file mode 100644 index 00000000..04ece8ae --- /dev/null +++ b/Test/dafny0/AnswerNoRuntimeChecking @@ -0,0 +1,328 @@ +
+-------------------- Simple --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+
+-------------------- TypeTests --------------------
+TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
+TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+34 resolution/type errors detected in TypeTests.dfy
+
+-------------------- NatTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- SmallTests --------------------
+Compilation error: an assume statement cannot be compiled (line 13)
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: an assume statement cannot be compiled (line 545)
+Compilation error: an assume statement cannot be compiled (line 554)
+Compilation error: an assume statement cannot be compiled (line 556)
+Compilation error: an assume statement cannot be compiled (line 559)
+Compilation error: an assume statement cannot be compiled (line 571)
+Compilation error: an assume statement cannot be compiled (line 574)
+Compilation error: an assume statement cannot be compiled (line 575)
+Compilation error: an assume statement cannot be compiled (line 577)
+Compilation error: an assume statement cannot be compiled (line 584)
+Compilation error: an assume statement cannot be compiled (line 590)
+Compilation error: an assume statement cannot be compiled (line 596)
+Compilation error: an assume statement cannot be compiled (line 603)
+
+-------------------- Definedness --------------------
+Compilation error: an assume statement cannot be compiled (line 93)
+
+-------------------- FunctionSpecifications --------------------
+Compiled assembly into FunctionSpecifications.dll
+
+-------------------- ResolutionErrors --------------------
+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
+ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(261,2): Error: duplicate label
+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+48 resolution/type errors detected in ResolutionErrors.dfy
+
+-------------------- ParseErrors --------------------
+ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
+ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
+ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
+ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
+8 parse errors detected in ParseErrors.dfy
+
+-------------------- Array --------------------
+Compilation error: Arbitrary type ('B') cannot be compiled
+
+-------------------- MultiDimArray --------------------
+Compiled assembly into MultiDimArray.dll
+
+-------------------- NonGhostQuantifiers --------------------
+NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+20 resolution/type errors detected in NonGhostQuantifiers.dfy
+
+-------------------- AdvancedLHS --------------------
+Compiled assembly into AdvancedLHS.dll
+
+-------------------- ModulesCycle --------------------
+ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
+ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+2 resolution/type errors detected in ModulesCycle.dfy
+
+-------------------- Modules0 --------------------
+Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(250,15): Error: unresolved identifier: X
+Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(294,16): Error: member R does not exist in class B
+Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
+30 resolution/type errors detected in Modules0.dfy
+
+-------------------- BadFunction --------------------
+Compiled assembly into BadFunction.dll
+
+-------------------- Comprehensions --------------------
+Compiled assembly into Comprehensions.exe
+
+-------------------- Basics --------------------
+Compilation error: an assume statement cannot be compiled (line 22)
+
+-------------------- ControlStructures --------------------
+Compiled assembly into ControlStructures.dll
+
+-------------------- DTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- ParallelResolveErrors --------------------
+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field
+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement
+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements
+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement
+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
+15 resolution/type errors detected in ParallelResolveErrors.dfy
+
+-------------------- Parallel --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: an assume statement cannot be compiled (line 47)
+
+-------------------- TypeParameters --------------------
+Compiled assembly into TypeParameters.exe
+
+-------------------- Coinductive --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
+
+-------------------- Corecursion --------------------
+Compiled assembly into Corecursion.dll
+
+-------------------- TypeAntecedents --------------------
+Compiled assembly into TypeAntecedents.exe
+
+-------------------- SplitExpr --------------------
+Compiled assembly into SplitExpr.dll
+
+-------------------- LoopModifies --------------------
+Compiled assembly into LoopModifies.dll
+
+-------------------- Refinement --------------------
+Compilation error: Method BodyFree._default.M has no body
+Compilation error: an assume statement cannot be compiled (line 128)
+
+-------------------- RefinementErrors --------------------
+RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions
+RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause
+RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate
+RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base
+RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
+RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')
+RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')
+RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')
+RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
+RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
+RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
+11 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- ReturnErrors --------------------
+ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
+ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
+3 resolution/type errors detected in ReturnErrors.dfy
+
+-------------------- ChainingDisjointTests --------------------
+Compiled assembly into ChainingDisjointTests.dll
+
+-------------------- CallStmtTests --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
+
+-------------------- MultiSets --------------------
+Compiled assembly into MultiSets.dll
+
+-------------------- PredExpr --------------------
+Compiled assembly into PredExpr.dll
+
+-------------------- LetExpr --------------------
+Compilation error: an assume statement cannot be compiled (line 31)
+Compilation error: an assume statement cannot be compiled (line 33)
+Compilation error: an assume statement cannot be compiled (line 34)
+
+-------------------- Skeletons --------------------
+Compilation error: an assume statement cannot be compiled (line 5)
+Compilation error: an assume statement cannot be compiled (line 7)
+
+-------------------- Maps --------------------
+Compiled assembly into Maps.exe
+
+-------------------- Compilation --------------------
+Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/AnswerRuntimeChecking b/Test/dafny0/AnswerRuntimeChecking new file mode 100644 index 00000000..e3970b78 --- /dev/null +++ b/Test/dafny0/AnswerRuntimeChecking @@ -0,0 +1,272 @@ +
+-------------------- Simple --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+
+-------------------- TypeTests --------------------
+TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
+TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+34 resolution/type errors detected in TypeTests.dfy
+
+-------------------- NatTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- Definedness --------------------
+Compiled assembly into Definedness.dll
+Rewrote assembly into Definedness.dll
+
+-------------------- FunctionSpecifications --------------------
+Compiled assembly into FunctionSpecifications.dll
+Rewrote assembly into FunctionSpecifications.dll
+
+-------------------- ResolutionErrors --------------------
+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
+ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(261,2): Error: duplicate label
+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+48 resolution/type errors detected in ResolutionErrors.dfy
+
+-------------------- ParseErrors --------------------
+ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
+ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
+ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
+ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
+8 parse errors detected in ParseErrors.dfy
+
+-------------------- Array --------------------
+Compilation error: Arbitrary type ('B') cannot be compiled
+
+-------------------- MultiDimArray --------------------
+Compiled assembly into MultiDimArray.dll
+Rewrote assembly into MultiDimArray.dll
+
+-------------------- NonGhostQuantifiers --------------------
+NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+20 resolution/type errors detected in NonGhostQuantifiers.dfy
+
+-------------------- ModulesCycle --------------------
+ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
+ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+2 resolution/type errors detected in ModulesCycle.dfy
+
+-------------------- Modules0 --------------------
+Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(250,15): Error: unresolved identifier: X
+Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(294,16): Error: member R does not exist in class B
+Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
+30 resolution/type errors detected in Modules0.dfy
+
+-------------------- Comprehensions --------------------
+Compiled assembly into Comprehensions.exe
+Rewrote assembly into Comprehensions.exe
+
+-------------------- ControlStructures --------------------
+Compiled assembly into ControlStructures.dll
+Rewrote assembly into ControlStructures.dll
+
+-------------------- ParallelResolveErrors --------------------
+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field
+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement
+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements
+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement
+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
+15 resolution/type errors detected in ParallelResolveErrors.dfy
+
+-------------------- Coinductive --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
+
+-------------------- Corecursion --------------------
+Compiled assembly into Corecursion.dll
+Rewrote assembly into Corecursion.dll
+
+-------------------- LoopModifies --------------------
+Compiled assembly into LoopModifies.dll
+Rewrote assembly into LoopModifies.dll
+
+-------------------- Refinement --------------------
+Compilation error: Method BodyFree._default.M has no body
+
+-------------------- RefinementErrors --------------------
+RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions
+RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause
+RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate
+RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base
+RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
+RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')
+RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')
+RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')
+RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
+RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
+RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
+11 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- ReturnErrors --------------------
+ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
+ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
+3 resolution/type errors detected in ReturnErrors.dfy
+
+-------------------- ChainingDisjointTests --------------------
+Compiled assembly into ChainingDisjointTests.dll
+Rewrote assembly into ChainingDisjointTests.dll
+
+-------------------- CallStmtTests --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
+
+-------------------- PredExpr --------------------
+Compiled assembly into PredExpr.dll
+Rewrote assembly into PredExpr.dll
+
+-------------------- Skeletons --------------------
+Compiled assembly into Skeletons.dll
+Rewrote assembly into Skeletons.dll
+
+-------------------- Compilation --------------------
+Compiled assembly into Compilation.exe
+Rewrote assembly into Compilation.exe
diff --git a/Test/dafny0/runtestNoRuntimeChecking.bat b/Test/dafny0/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..c90930d5 --- /dev/null +++ b/Test/dafny0/runtestNoRuntimeChecking.bat @@ -0,0 +1,44 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM Modules1
+REM Termination
+REM Datatypes
+REM NoTypeArgs
+REM ReturnTests
+REM Predicates
+
+for %%f in (Simple TypeTests NatTypes SmallTests Definedness
+ FunctionSpecifications ResolutionErrors ParseErrors
+ Array MultiDimArray NonGhostQuantifiers AdvancedLHS
+ ModulesCycle Modules0 BadFunction Comprehensions
+ Basics ControlStructures DTypes ParallelResolveErrors
+ Parallel TypeParameters Coinductive Corecursion
+ TypeAntecedents SplitExpr LoopModifies Refinement
+ RefinementErrors ReturnErrors ChainingDisjointTests
+ CallStmtTests MultiSets PredExpr LetExpr Skeletons
+ Maps Compilation) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny0/runtestRuntimeChecking.bat b/Test/dafny0/runtestRuntimeChecking.bat new file mode 100644 index 00000000..42d21010 --- /dev/null +++ b/Test/dafny0/runtestRuntimeChecking.bat @@ -0,0 +1,55 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM Modules1
+REM Termination
+REM Datatypes
+REM NoTypeArgs
+REM ReturnTests
+REM Predicates
+
+REM to implement:
+REM SmallTests : unexpected expressions
+REM AdvancedLHS : fresh expressions
+REM BadFunction : ghost state
+REM Basics : ghost state
+REM DTypes : quantifiers
+REM Parallel : quantifiers
+REM TypeParameters : ghost state
+REM TypeAntecedents: quantifiers
+REM SplitExpr : ghost state
+REM MultiSets : quantifiers
+REM LetExpr : old expressions
+REM Maps : quantifiers
+
+for %%f in (Simple TypeTests NatTypes Definedness
+ FunctionSpecifications ResolutionErrors ParseErrors
+ Array MultiDimArray NonGhostQuantifiers ModulesCycle
+ Modules0 Comprehensions ControlStructures ParallelResolveErrors
+ Coinductive Corecursion LoopModifies Refinement
+ RefinementErrors ReturnErrors ChainingDisjointTests
+ CallStmtTests PredExpr Skeletons Compilation) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking new file mode 100644 index 00000000..5472ec14 --- /dev/null +++ b/Test/dafny1/AnswerNoRuntimeChecking @@ -0,0 +1,76 @@ +
+-------------------- Queue --------------------
+Compiled assembly into Queue.dll
+
+-------------------- PriorityQueue --------------------
+Compiled assembly into PriorityQueue.dll
+
+-------------------- ExtensibleArray --------------------
+Compiled assembly into ExtensibleArray.exe
+
+-------------------- ExtensibleArrayAuto --------------------
+Compiled assembly into ExtensibleArrayAuto.exe
+
+-------------------- BinaryTree --------------------
+Compiled assembly into BinaryTree.dll
+
+-------------------- UnboundedStack --------------------
+Compiled assembly into UnboundedStack.dll
+
+-------------------- ListCopy --------------------
+Compilation error: an assume statement cannot be compiled (line 14)
+Compilation error: an assume statement cannot be compiled (line 15)
+
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+
+-------------------- ListContents --------------------
+Compiled assembly into ListContents.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+
+-------------------- SchorrWaite --------------------
+Compiled assembly into SchorrWaite.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+
+-------------------- SumOfCubes --------------------
+Compiled assembly into SumOfCubes.dll
+
+-------------------- FindZero --------------------
+Compiled assembly into FindZero.dll
+
+-------------------- TerminationDemos --------------------
+Compiled assembly into TerminationDemos.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compilation error: an assume statement cannot be compiled (line 66)
+
+-------------------- Induction --------------------
+Compiled assembly into Induction.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
+
+-------------------- Celebrity --------------------
+Compilation error: Function _default._default.Knows has no body
+Compilation error: an assume statement cannot be compiled (line 16)
+
+-------------------- BDD --------------------
+Compiled assembly into BDD.dll
+
+-------------------- UltraFilter --------------------
+Compilation error: Method _default.UltraFilter.H has no body
+Compilation error: an assume statement cannot be compiled (line 42)
+Compilation error: an assume statement cannot be compiled (line 45)
+Compilation error: an assume statement cannot be compiled (line 76)
+Compilation error: an assume statement cannot be compiled (line 97)
+Compilation error: an assume statement cannot be compiled (line 98)
diff --git a/Test/dafny1/AnswerRuntimeChecking b/Test/dafny1/AnswerRuntimeChecking new file mode 100644 index 00000000..1ade5aeb --- /dev/null +++ b/Test/dafny1/AnswerRuntimeChecking @@ -0,0 +1,27 @@ +
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+Rewrote assembly into ListReverse.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+Rewrote assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+Rewrote assembly into pow2.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+Rewrote assembly into Cubes.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+Rewrote assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compiled assembly into KatzManna.dll
+Rewrote assembly into KatzManna.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
diff --git a/Test/dafny1/runtestNoRuntimeChecking.bat b/Test/dafny1/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..a4989fa1 --- /dev/null +++ b/Test/dafny1/runtestNoRuntimeChecking.bat @@ -0,0 +1,36 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+for %%f in (Queue PriorityQueue ExtensibleArray ExtensibleArrayAuto
+ BinaryTree UnboundedStack ListCopy ListReverse ListContents
+ MatrixFun pow2 SchorrWaite Cubes SumOfCubes FindZero
+ TerminationDemos Substitution KatzManna Induction Rippling
+ Celebrity BDD UltraFilter) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny1/runtestRuntimeChecking.bat b/Test/dafny1/runtestRuntimeChecking.bat new file mode 100644 index 00000000..fc32fbf4 --- /dev/null +++ b/Test/dafny1/runtestRuntimeChecking.bat @@ -0,0 +1,51 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+REM to implement:
+REM Queue : parallel statements
+REM PriorityQueue : ghost state
+REM ExtensibleArray : ghost state
+REM ExtensibleArrayAuto: ghost state
+REM BinaryTree : old expressions
+REM UnboundedStack : ghost state
+REM ListCopy : fresh expressions
+REM ListContents : old expressions
+REM SchorrWaite : ghost state
+REM SumOfCubes : ghost state
+REM FindZero : ghost state
+REM TerminationDemos : ghost state
+REM Induction : quantifiers
+REM Celebrity : quantifiers
+REM BDD : ghost state
+REM UltraFilter : quantifiers
+
+for %%f in (ListReverse MatrixFun pow2 Cubes Substitution KatzManna
+ Rippling) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny2/AnswerNoRuntimeChecking b/Test/dafny2/AnswerNoRuntimeChecking new file mode 100644 index 00000000..f04bb934 --- /dev/null +++ b/Test/dafny2/AnswerNoRuntimeChecking @@ -0,0 +1,30 @@ +
+-------------------- Classics --------------------
+Compiled assembly into Classics.dll
+
+-------------------- TreeBarrier --------------------
+Compilation error: an assume statement cannot be compiled (line 90)
+Compilation error: an assume statement cannot be compiled (line 102)
+Compilation error: an assume statement cannot be compiled (line 128)
+
+-------------------- COST-verif-comp-2011-1-MaxArray --------------------
+Compiled assembly into COST-verif-comp-2011-1-MaxArray.dll
+
+-------------------- COST-verif-comp-2011-2-MaxTree-class --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-class.dll
+
+-------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+
+-------------------- COST-verif-comp-2011-3-TwoDuplicates --------------------
+Compiled assembly into COST-verif-comp-2011-3-TwoDuplicates.dll
+
+-------------------- COST-verif-comp-2011-4-FloydCycleDetect --------------------
+Compiled assembly into COST-verif-comp-2011-4-FloydCycleDetect.dll
+
+-------------------- Intervals --------------------
+Compiled assembly into Intervals.dll
+
+-------------------- StoreAndRetrieve --------------------
+Compilation error: an assume statement cannot be compiled (line 21)
+Compilation error: Function Library.Function.Apply has no body
diff --git a/Test/dafny2/AnswerRuntimeChecking b/Test/dafny2/AnswerRuntimeChecking new file mode 100644 index 00000000..32b61bb1 --- /dev/null +++ b/Test/dafny2/AnswerRuntimeChecking @@ -0,0 +1,7 @@ +
+-------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+Rewrote assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+
+-------------------- StoreAndRetrieve --------------------
+Compilation error: Function Library.Function.Apply has no body
diff --git a/Test/dafny2/runtestNoRuntimeChecking.bat b/Test/dafny2/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..b60fd69c --- /dev/null +++ b/Test/dafny2/runtestNoRuntimeChecking.bat @@ -0,0 +1,34 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM soon again: SnapshotableTrees.dfy
+
+for %%f in (Classics TreeBarrier COST-verif-comp-2011-1-MaxArray
+ COST-verif-comp-2011-2-MaxTree-class
+ COST-verif-comp-2011-2-MaxTree-datatype
+ COST-verif-comp-2011-3-TwoDuplicates
+ COST-verif-comp-2011-4-FloydCycleDetect
+ Intervals StoreAndRetrieve) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny2/runtestRuntimeChecking.bat b/Test/dafny2/runtestRuntimeChecking.bat new file mode 100644 index 00000000..4ba447a7 --- /dev/null +++ b/Test/dafny2/runtestRuntimeChecking.bat @@ -0,0 +1,39 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM soon again: SnapshotableTrees.dfy
+
+REM to implement:
+REM Classics : ghost state
+REM TreeBarrier : ghost state
+REM COST-verif-comp-2011-1-MaxArray : ghost state
+REM COST-verif-comp-2011-2-MaxTree-class : ghost state
+REM COST-verif-comp-2011-3-TwoDuplicates : quantifiers
+REM COST-verif-comp-2011-4-FloydCycleDetect: quantifiers
+REM Intervals : ghost state
+
+for %%f in (COST-verif-comp-2011-2-MaxTree-datatype
+ StoreAndRetrieve) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafnyCompiler/Answer b/Test/dafnyCompiler/Answer new file mode 100644 index 00000000..11e295fc --- /dev/null +++ b/Test/dafnyCompiler/Answer @@ -0,0 +1,32 @@ +----- Running regression test ..\dafny0 (without runtime checking)
+..\dafny0 Succeeded
+----- Running regression test ..\dafny1 (without runtime checking)
+..\dafny1 Succeeded
+----- Running regression test ..\dafny2 (without runtime checking)
+..\dafny2 Succeeded
+----- Running regression test ..\dafnyRuntimeChecking (without runtime checking)
+..\dafnyRuntimeChecking Succeeded
+----- Running regression test ..\VSI-Benchmarks (without runtime checking)
+..\VSI-Benchmarks Succeeded
+----- Running regression test ..\vacid0 (without runtime checking)
+..\vacid0 Succeeded
+----- Running regression test ..\vstte2012 (without runtime checking)
+..\vstte2012 Succeeded
+----- Running regression test ..\VSComp2010 (without runtime checking)
+..\VSComp2010 Succeeded
+----- Running regression test ..\dafny0 (with runtime checking)
+..\dafny0 Succeeded
+----- Running regression test ..\dafny1 (with runtime checking)
+..\dafny1 Succeeded
+----- Running regression test ..\dafny2 (with runtime checking)
+..\dafny2 Succeeded
+----- Running regression test ..\dafnyRuntimeChecking (with runtime checking)
+..\dafnyRuntimeChecking Succeeded
+----- Running regression test ..\VSI-Benchmarks (with runtime checking)
+..\VSI-Benchmarks Succeeded
+----- Running regression test ..\vacid0 (with runtime checking)
+..\vacid0 Succeeded
+----- Running regression test ..\vstte2012 (with runtime checking)
+..\vstte2012 Succeeded
+----- Running regression test ..\VSComp2010 (with runtime checking)
+..\VSComp2010 Succeeded
diff --git a/Test/dafnyCompiler/compilerTests.txt b/Test/dafnyCompiler/compilerTests.txt new file mode 100644 index 00000000..6b3abbd4 --- /dev/null +++ b/Test/dafnyCompiler/compilerTests.txt @@ -0,0 +1,8 @@ +..\dafny0 Use Dafny functionality tests
+..\dafny1 Use Various Dafny examples
+..\dafny2 Use More Dafny examples
+..\dafnyRuntimeChecking Use Dafny runtime checking tests
+..\VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
+..\vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
+..\vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
+..\VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
diff --git a/Test/dafnyCompiler/runtest.bat b/Test/dafnyCompiler/runtest.bat new file mode 100644 index 00000000..0df12552 --- /dev/null +++ b/Test/dafnyCompiler/runtest.bat @@ -0,0 +1,56 @@ +@echo off
+rem Usage: runtest.bat <dir> [runtimeChecking]
+if "%1" == "" goto noDirSpecified
+if "%1" == "runtimeChecking" goto noDirSpecified
+if not exist %1\nul goto noDirExists
+pushd %1
+if "%2" == "runtimeChecking" goto RuntimeChecking
+:NoRuntimeChecking
+echo ----- Running regression test %1 (without runtime checking)
+if not exist runtestNoRuntimeChecking.bat goto noRunTestNoRuntimeChecking
+call runtestNoRuntimeChecking.bat -nologo -logPrefix:%1 > OutputNoRuntimeChecking
+rem There seem to be some race between finishing writing to the Output file, and running fc.
+rem Calling fc twice seems to fix (or at least alleviate) the problem.
+fc /W AnswerNoRuntimeChecking OutputNoRuntimeChecking > nul
+fc /W AnswerNoRuntimeChecking OutputNoRuntimeChecking > nul
+goto Continue
+:RuntimeChecking
+echo ----- Running regression test %1 (with runtime checking)
+if not exist runtestRuntimeChecking.bat goto noRunTestRuntimeChecking
+call runtestRuntimeChecking.bat -nologo -logPrefix:%1 > OutputRuntimeChecking
+rem There seem to be some race between finishing writing to the Output file, and running fc.
+rem Calling fc twice seems to fix (or at least alleviate) the problem.
+fc /W AnswerRuntimeChecking OutputRuntimeChecking > nul
+fc /W AnswerRuntimeChecking OutputRuntimeChecking > nul
+:Continue
+if not errorlevel 1 goto passTest
+echo %1 FAILED
+goto errorEnd
+
+:passTest
+echo %1 Succeeded
+goto end
+
+:noDirSpecified
+echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ]
+goto errorEnd
+
+:noDirExists
+echo runtest: Error: There is no test directory %1
+goto errorEnd
+
+:noRunTestNoRuntimeChecking
+echo runtest: Error: no runtestNoRuntimeChecking.bat found in test directory %1
+goto errorEnd
+
+:noRunTestRuntimeChecking
+echo runtest: Error: no runtestRuntimeChecking.bat found in test directory %1
+goto errorEnd
+
+:errorEnd
+popd
+exit /b 1
+
+:end
+popd
+exit /b 0
diff --git a/Test/dafnyCompiler/runtestall.bat b/Test/dafnyCompiler/runtestall.bat new file mode 100644 index 00000000..a0446aa3 --- /dev/null +++ b/Test/dafnyCompiler/runtestall.bat @@ -0,0 +1,10 @@ +@echo off
+setlocal
+
+set errors=0
+
+for /F "eol=; tokens=1,2,3*" %%i in (compilerTests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1
+
+for /F "eol=; tokens=1,2,3*" %%i in (compilerTests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 runtimeChecking || set errors=1
+
+exit /b %errors%
diff --git a/Test/dafnyRuntimeChecking/Answer b/Test/dafnyRuntimeChecking/Answer new file mode 100644 index 00000000..0cc946ab --- /dev/null +++ b/Test/dafnyRuntimeChecking/Answer @@ -0,0 +1,4826 @@ +
+-------------------- AssumeStmt0 --------------------
+Compiled program written to AssumeStmt0.cs
+Compiled assembly into AssumeStmt0.exe
+Rewrote assembly into AssumeStmt0.exe
+// Dafny program AssumeStmt0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Assume((new BigInteger(2)) < (new BigInteger(10)));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- AssumeStmt1 --------------------
+Compiled program written to AssumeStmt1.cs
+Compiled assembly into AssumeStmt1.exe
+Rewrote assembly into AssumeStmt1.exe
+// Dafny program AssumeStmt1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Assume((new BigInteger(10)) < (new BigInteger(2)));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- AssertStmt0 --------------------
+Compiled program written to AssertStmt0.cs
+Compiled assembly into AssertStmt0.exe
+Rewrote assembly into AssertStmt0.exe
+// Dafny program AssertStmt0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Assert((new BigInteger(2)) < (new BigInteger(10)));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- AssertStmt1 --------------------
+Compiled program written to AssertStmt1.cs
+Compiled assembly into AssertStmt1.exe
+Rewrote assembly into AssertStmt1.exe
+// Dafny program AssertStmt1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Assert((new BigInteger(10)) < (new BigInteger(2)));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- Precondition0 --------------------
+Compiled program written to Precondition0.cs
+Compiled assembly into Precondition0.exe
+Rewrote assembly into Precondition0.exe
+// Dafny program Precondition0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Requires(true);
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- Precondition1 --------------------
+Compiled program written to Precondition1.cs
+Compiled assembly into Precondition1.exe
+Rewrote assembly into Precondition1.exe
+// Dafny program Precondition1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @foo(BigInteger @x, BigInteger @y)
+ {
+ Contract.Requires((new BigInteger(0)) <= (@x));
+ Contract.Requires((@y) <= (new BigInteger(0)));
+ }
+ public void @Main()
+ {
+ (this).@foo(new BigInteger(2), (new BigInteger(0)) - (new BigInteger(7)));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- Postcondition0 --------------------
+Compiled program written to Postcondition0.cs
+Compiled assembly into Postcondition0.exe
+Rewrote assembly into Postcondition0.exe
+// Dafny program Postcondition0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public void @Main()
+ {
+ Contract.Ensures(true);
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
+
+-------------------- Postcondition1 --------------------
+Compiled program written to Postcondition1.cs
+Compiled assembly into Postcondition1.exe
+Rewrote assembly into Postcondition1.exe
+// Dafny program Postcondition1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @__default {
+ public BigInteger @x = new BigInteger(0);
+ public BigInteger @y = new BigInteger(0);
+ public void @Main()
+ {
+ Contract.Ensures((new BigInteger(0)) <= ((this).@x));
+ Contract.Ensures(((this).@y) <= (new BigInteger(0)));
+ (this).@x = new BigInteger(2);
+ (this).@y = (new BigInteger(0)) - (new BigInteger(7));
+ }
+ public static void Main(string[] args) {
+ @__default b = new @__default();
+ b.Main();
+ }
+}
diff --git a/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking b/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking new file mode 100644 index 00000000..6fffd815 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking @@ -0,0 +1,24 @@ +
+-------------------- AssumeStmt0 --------------------
+Compilation error: an assume statement cannot be compiled (line 3)
+
+-------------------- AssumeStmt1 --------------------
+Compilation error: an assume statement cannot be compiled (line 3)
+
+-------------------- AssertStmt0 --------------------
+Compiled assembly into AssertStmt0.exe
+
+-------------------- AssertStmt1 --------------------
+Compiled assembly into AssertStmt1.exe
+
+-------------------- Precondition0 --------------------
+Compiled assembly into Precondition0.exe
+
+-------------------- Precondition1 --------------------
+Compiled assembly into Precondition1.exe
+
+-------------------- Postcondition0 --------------------
+Compiled assembly into Postcondition0.exe
+
+-------------------- Postcondition1 --------------------
+Compiled assembly into Postcondition1.exe
diff --git a/Test/dafnyRuntimeChecking/AnswerRuntimeChecking b/Test/dafnyRuntimeChecking/AnswerRuntimeChecking new file mode 100644 index 00000000..860dc843 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AnswerRuntimeChecking @@ -0,0 +1,32 @@ +
+-------------------- AssumeStmt0 --------------------
+Compiled assembly into AssumeStmt0.exe
+Rewrote assembly into AssumeStmt0.exe
+
+-------------------- AssumeStmt1 --------------------
+Compiled assembly into AssumeStmt1.exe
+Rewrote assembly into AssumeStmt1.exe
+
+-------------------- AssertStmt0 --------------------
+Compiled assembly into AssertStmt0.exe
+Rewrote assembly into AssertStmt0.exe
+
+-------------------- AssertStmt1 --------------------
+Compiled assembly into AssertStmt1.exe
+Rewrote assembly into AssertStmt1.exe
+
+-------------------- Precondition0 --------------------
+Compiled assembly into Precondition0.exe
+Rewrote assembly into Precondition0.exe
+
+-------------------- Precondition1 --------------------
+Compiled assembly into Precondition1.exe
+Rewrote assembly into Precondition1.exe
+
+-------------------- Postcondition0 --------------------
+Compiled assembly into Postcondition0.exe
+Rewrote assembly into Postcondition0.exe
+
+-------------------- Postcondition1 --------------------
+Compiled assembly into Postcondition1.exe
+Rewrote assembly into Postcondition1.exe
diff --git a/Test/dafnyRuntimeChecking/AssertStmt0.dfy b/Test/dafnyRuntimeChecking/AssertStmt0.dfy new file mode 100644 index 00000000..5596e9e9 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssertStmt0.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assert 2 < 10;
+}
diff --git a/Test/dafnyRuntimeChecking/AssertStmt1.dfy b/Test/dafnyRuntimeChecking/AssertStmt1.dfy new file mode 100644 index 00000000..2730e87c --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssertStmt1.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assert 10 < 2;
+}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt0.dfy b/Test/dafnyRuntimeChecking/AssumeStmt0.dfy new file mode 100644 index 00000000..13f58deb --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssumeStmt0.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assume 2 < 10;
+}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt1.dfy b/Test/dafnyRuntimeChecking/AssumeStmt1.dfy new file mode 100644 index 00000000..7a749f51 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssumeStmt1.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assume 10 < 2;
+}
diff --git a/Test/dafnyRuntimeChecking/Postcondition0.dfy b/Test/dafnyRuntimeChecking/Postcondition0.dfy new file mode 100644 index 00000000..5b61988c --- /dev/null +++ b/Test/dafnyRuntimeChecking/Postcondition0.dfy @@ -0,0 +1,3 @@ +method Main()
+ ensures true;
+{}
diff --git a/Test/dafnyRuntimeChecking/Postcondition1.dfy b/Test/dafnyRuntimeChecking/Postcondition1.dfy new file mode 100644 index 00000000..0969c51d --- /dev/null +++ b/Test/dafnyRuntimeChecking/Postcondition1.dfy @@ -0,0 +1,11 @@ +var x: int;
+var y: int;
+
+method Main()
+ modifies this`x, this`y;
+ ensures 0 <= x;
+ ensures y <= 0;
+{
+ x := 2;
+ y := -7;
+}
diff --git a/Test/dafnyRuntimeChecking/Precondition0.dfy b/Test/dafnyRuntimeChecking/Precondition0.dfy new file mode 100644 index 00000000..73733bbb --- /dev/null +++ b/Test/dafnyRuntimeChecking/Precondition0.dfy @@ -0,0 +1,3 @@ +method Main()
+ requires true;
+{}
diff --git a/Test/dafnyRuntimeChecking/Precondition1.dfy b/Test/dafnyRuntimeChecking/Precondition1.dfy new file mode 100644 index 00000000..1732b0bc --- /dev/null +++ b/Test/dafnyRuntimeChecking/Precondition1.dfy @@ -0,0 +1,9 @@ +method foo(x: int, y: int)
+ requires 0 <= x;
+ requires y <= 0;
+{}
+
+method Main()
+{
+ foo(2, -7);
+}
diff --git a/Test/dafnyRuntimeChecking/runtest.bat b/Test/dafnyRuntimeChecking/runtest.bat new file mode 100644 index 00000000..3e434f49 --- /dev/null +++ b/Test/dafnyRuntimeChecking/runtest.bat @@ -0,0 +1,26 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1
+ Precondition0 Precondition1 Postcondition0 Postcondition1) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 /spillTargetCode:1 %* %%f.dfy
+ if exist %%f.cs. (
+ type %%f.cs
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat b/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..e336e022 --- /dev/null +++ b/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat @@ -0,0 +1,25 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1
+ Precondition0 Precondition1 Postcondition0 Postcondition1) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat b/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat new file mode 100644 index 00000000..6b086f6f --- /dev/null +++ b/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat @@ -0,0 +1,25 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1
+ Precondition0 Precondition1 Postcondition0 Postcondition1) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafnytests.txt b/Test/dafnytests.txt index 2b457c91..ca40465e 100644 --- a/Test/dafnytests.txt +++ b/Test/dafnytests.txt @@ -1,7 +1,9 @@ -dafny0 Use Dafny functionality tests
-dafny1 Use Various Dafny examples
-dafny2 Use More Dafny examples
-VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
-vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
-vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
-VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
+dafny0 Use Dafny functionality tests
+dafny1 Use Various Dafny examples
+dafny2 Use More Dafny examples
+dafnyRuntimeChecking Use Dafny runtime checking tests
+dafnyCompiler Postpone Dafny compiler tests
+VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
+vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
+vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
+VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
diff --git a/Test/runtest.bat b/Test/runtest.bat index 5b3d45ae..8a75f363 100644 --- a/Test/runtest.bat +++ b/Test/runtest.bat @@ -5,7 +5,12 @@ if not exist %1\nul goto noDirExists echo ----- Running regression test %1
pushd %1
if not exist runtest.bat goto noRunTest
+if "%1" == "dafnyCompiler" goto compilerTests
call runtest.bat -nologo -logPrefix:%* > Output
+goto Continue
+:compilerTests
+call runtestall.bat > Output
+:Continue
rem There seem to be some race between finishing writing to the Output file, and running fc.
rem Calling fc twice seems to fix (or at least alleviate) the problem.
fc /W Answer Output > nul
diff --git a/Test/vacid0/AnswerNoRuntimeChecking b/Test/vacid0/AnswerNoRuntimeChecking new file mode 100644 index 00000000..a1f7f57b --- /dev/null +++ b/Test/vacid0/AnswerNoRuntimeChecking @@ -0,0 +1,9 @@ +
+-------------------- LazyInitArray --------------------
+Compiled assembly into LazyInitArray.dll
+
+-------------------- SparseArray --------------------
+Compiled assembly into SparseArray.dll
+
+-------------------- Composite --------------------
+Compiled assembly into Composite.exe
diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/Test/vacid0/AnswerRuntimeChecking diff --git a/Test/vacid0/runtestNoRuntimeChecking.bat b/Test/vacid0/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..3a7befa2 --- /dev/null +++ b/Test/vacid0/runtestNoRuntimeChecking.bat @@ -0,0 +1,27 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (LazyInitArray SparseArray Composite) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vacid0/runtestRuntimeChecking.bat b/Test/vacid0/runtestRuntimeChecking.bat new file mode 100644 index 00000000..077c1002 --- /dev/null +++ b/Test/vacid0/runtestRuntimeChecking.bat @@ -0,0 +1,32 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM LazyInitArray: ghost state
+REM SparseArray : ghost state
+REM Composite : ghost state
+
+for %%f in () do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vstte2012/AnswerNoRuntimeChecking b/Test/vstte2012/AnswerNoRuntimeChecking new file mode 100644 index 00000000..c5508749 --- /dev/null +++ b/Test/vstte2012/AnswerNoRuntimeChecking @@ -0,0 +1,18 @@ +
+-------------------- Two-Way-Sort --------------------
+Compiled assembly into Two-Way-Sort.dll
+
+-------------------- Combinators --------------------
+Compiled assembly into Combinators.dll
+
+-------------------- RingBuffer --------------------
+Compiled assembly into RingBuffer.dll
+
+-------------------- RingBufferAuto --------------------
+Compiled assembly into RingBufferAuto.dll
+
+-------------------- Tree --------------------
+Compiled assembly into Tree.dll
+
+-------------------- BreadthFirstSearch --------------------
+Compilation error: Function _default.BreadthFirstSearch.Succ has no body
diff --git a/Test/vstte2012/AnswerRuntimeChecking b/Test/vstte2012/AnswerRuntimeChecking new file mode 100644 index 00000000..5c703cc7 --- /dev/null +++ b/Test/vstte2012/AnswerRuntimeChecking @@ -0,0 +1,11 @@ +
+-------------------- Two-Way-Sort --------------------
+Compiled assembly into Two-Way-Sort.dll
+Rewrote assembly into Two-Way-Sort.dll
+
+-------------------- Tree --------------------
+Compiled assembly into Tree.dll
+Rewrote assembly into Tree.dll
+
+-------------------- BreadthFirstSearch --------------------
+Compilation error: Function _default.BreadthFirstSearch.Succ has no body
diff --git a/Test/vstte2012/runtestNoRuntimeChecking.bat b/Test/vstte2012/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..e572ed2f --- /dev/null +++ b/Test/vstte2012/runtestNoRuntimeChecking.bat @@ -0,0 +1,28 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (Two-Way-Sort Combinators RingBuffer RingBufferAuto
+ Tree BreadthFirstSearch) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vstte2012/runtestRuntimeChecking.bat b/Test/vstte2012/runtestRuntimeChecking.bat new file mode 100644 index 00000000..042efe96 --- /dev/null +++ b/Test/vstte2012/runtestRuntimeChecking.bat @@ -0,0 +1,32 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM Combinators : ghost state
+REM RingBuffer : ghost state
+REM RingBufferAuto: ghost state
+
+for %%f in (Two-Way-Sort Tree BreadthFirstSearch) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
|