diff options
| author |  afd <unknown> | 2012-06-27 14:49:15 +0100 |
|---|---|---|
| committer | afd <unknown> | 2012-06-27 14:49:15 +0100 |
| commit | c560dcbd38109b10ca93483379484ede395837e8 (patch) | |
| tree | bc7b411285800fcc5869f91ad89a311f29a9033b | |
| parent | 901bead882f3a221f073d98de2255de22f599b9a (diff) | |
Undo bad merge.
52 files changed, 32 insertions, 6803 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index fa8ea6da..e72c04dd 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -42,7 +42,6 @@ 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)
@@ -416,7 +415,7 @@ namespace Microsoft.Dafny { }
}
wr.Write(")");
-
+
wr.WriteLine(";");
Indent(ind + 2 * IndentAmount);
wr.WriteLine("}");
@@ -574,8 +573,6 @@ 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);
@@ -855,20 +852,12 @@ namespace Microsoft.Dafny { void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
- if (!DafnyOptions.O.RuntimeChecking && stmt.IsGhost) {
+ if (stmt.IsGhost) {
CheckHasNoAssumes(stmt);
return;
}
- if (stmt is AssumeStmt)
- {
- TrAssumeStmt((AssumeStmt)stmt, indent);
- }
- else if (stmt is AssertStmt)
- {
- TrAssertStmt((AssertStmt)stmt, indent);
- }
- else if (stmt is PrintStmt) {
+ if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (Attributes.Argument arg in s.Args) {
SpillLetVariableDecls(arg.E, indent);
@@ -2221,107 +2210,5 @@ 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 cb126446..34fa0487 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -33,8 +33,6 @@ 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
@@ -92,22 +90,6 @@ 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;
}
@@ -166,13 +148,6 @@ 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 2f7175f4..3534dcbf 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -23,7 +23,6 @@ namespace Microsoft.Dafny using VC;
using System.CodeDom.Compiler;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Win32; // needed for ccrewrite
public class DafnyDriver
{
@@ -151,7 +150,7 @@ namespace Microsoft.Dafny if (err != null) {
exitValue = ExitValue.DAFNY_ERROR;
ErrorWriteLine(err);
- } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck && DafnyOptions.O.Verification) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
@@ -188,14 +187,6 @@ 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;
}
@@ -240,33 +231,10 @@ 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) {
@@ -819,56 +787,5 @@ 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/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 018917d5..966f98eb 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -44,8 +44,6 @@ namespace GPUVerify public static bool InterGroupRaceChecking = false;
- public static bool BarrierParameters = false;
-
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -193,11 +191,6 @@ namespace GPUVerify InterGroupRaceChecking = true;
break;
- case "-barrierParameters":
- case "/barrierParameters":
- BarrierParameters = true;
- break;
-
default:
inputFiles.Add(args[i]);
break;
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 7cb7844f..e3d94fcc 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -58,9 +58,6 @@ namespace GPUVerify internal static Constant _NUM_GROUPS_Y = null;
internal static Constant _NUM_GROUPS_Z = null;
- internal const int CLK_LOCAL_MEM_FENCE = 1;
- internal const int CLK_GLOBAL_MEM_FENCE = 2;
-
public IRaceInstrumenter RaceInstrumenter;
public UniformityAnalyser uniformityAnalyser;
@@ -1453,13 +1450,8 @@ namespace GPUVerify BigBlock checkNonDivergence = new BigBlock(tok, "__BarrierImpl", new CmdSeq(), null, null);
bigblocks.Add(checkNonDivergence);
- Debug.Assert((BarrierProcedure.InParams.Length % 2) == 0);
- int paramsPerThread = BarrierProcedure.InParams.Length / 2;
IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));
- IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread].TypedIdent));
-
- IdentifierExpr Flags1 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent)) : null;
- IdentifierExpr Flags2 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread + 1].TypedIdent)) : null;
+ IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));
Expr DivergenceCondition = Expr.Eq(P1, P2);
if (CommandLineOptions.InterGroupRaceChecking)
@@ -1474,64 +1466,38 @@ namespace GPUVerify List<BigBlock> returnbigblocks = new List<BigBlock>();
returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));
StmtList returnstatement = new StmtList(returnbigblocks, BarrierProcedure.tok);
-
- Expr IfGuard;
-
- if (CommandLineOptions.InterGroupRaceChecking)
- {
- IfGuard = Expr.Or(Expr.And(Expr.Not(P1), Expr.Not(P2)), Expr.And(ThreadsInSameGroup(), Expr.Or(Expr.Not(P1), Expr.Not(P2))));
- }
- else
- {
- // We make this an "Or", not an "And", because "And" is implied by the assertion that the variables
- // are equal, together with the "Or". The weaker "Or" ensures that many auxiliary assertions will not
- // fail if divergence has not been proved.
- IfGuard = Expr.Or(Expr.Not(P1), Expr.Not(P2));
- }
- checkNonDivergence.ec = new IfCmd(tok, IfGuard, returnstatement, null, null);
+ // We make this an "Or", not an "And", because "And" is implied by the assertion that the variables
+ // are equal, together with the "Or". The weaker "Or" ensures that many auxiliary assertions will not
+ // fail if divergence has not been proved.
+ checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
}
+ if (CommandLineOptions.InterGroupRaceChecking)
{
- Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;
- Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;
-
- if (CommandLineOptions.BarrierParameters)
- {
- IfGuard1 = Expr.And(IfGuard1, CLK_LOCAL_MEM_FENCE_isSet(Flags1));
- IfGuard2 = Expr.And(IfGuard2, CLK_LOCAL_MEM_FENCE_isSet(Flags2));
- }
-
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, P1, new StmtList(MakeResetAndHavocBlocks(1), Token.NoToken), null, null),
null));
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, P2, new StmtList(MakeResetAndHavocBlocks(2), Token.NoToken), null, null),
null));
}
-
+ else
{
- Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;
- Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;
-
- if (CommandLineOptions.BarrierParameters)
+ foreach (BigBlock bb in MakeResetAndHavocBlocks(1))
{
- IfGuard1 = Expr.And(IfGuard1, CLK_GLOBAL_MEM_FENCE_isSet(Flags1));
- IfGuard2 = Expr.And(IfGuard2, CLK_GLOBAL_MEM_FENCE_isSet(Flags2));
+ bigblocks.Add(bb);
+ }
+ foreach (BigBlock bb in MakeResetAndHavocBlocks(2))
+ {
+ bigblocks.Add(bb);
}
-
- bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),
- null));
- bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),
- null));
}
foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
if (!ArrayModelledAdversarially(v))
{
- bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, Flags1, Flags2));
+ bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2));
}
}
@@ -1549,27 +1515,10 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(BarrierImplementation);
}
- private static Expr flagIsSet(Expr Flags, int flag)
- {
- return Expr.Eq(new BvExtractExpr(
- Token.NoToken, Flags, flag, flag - 1),
- new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));
- }
-
- private static Expr CLK_GLOBAL_MEM_FENCE_isSet(Expr Flags)
- {
- return flagIsSet(Flags, CLK_GLOBAL_MEM_FENCE);
- }
-
- private static Expr CLK_LOCAL_MEM_FENCE_isSet(Expr Flags)
- {
- return flagIsSet(Flags, CLK_LOCAL_MEM_FENCE);
- }
-
- private List<BigBlock> MakeResetAndHavocBlocks(int Thread, ICollection<Variable> variables)
+ private List<BigBlock> MakeResetAndHavocBlocks(int Thread)
{
List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();
- foreach (Variable v in variables)
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread));
if (!ArrayModelledAdversarially(v))
@@ -1616,36 +1565,18 @@ namespace GPUVerify return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new HavocCmd(Token.NoToken, new IdentifierExprSeq(new IdentifierExpr[] { vForThread })) }), null, null);
}
- private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2, Expr Flags1, Expr Flags2)
+ private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2)
{
IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
Expr AssumeGuard = Expr.Eq(v1, v2);
- Expr EqualityCondition = Expr.True;
-
if (CommandLineOptions.InterGroupRaceChecking)
{
- EqualityCondition = ThreadsInSameGroup();
+ AssumeGuard = Expr.Imp(ThreadsInSameGroup(), AssumeGuard);
}
- if (CommandLineOptions.BarrierParameters)
- {
- if (NonLocalState.getGroupSharedVariables().Contains(v))
- {
- EqualityCondition = Expr.And(EqualityCondition,
- Expr.And(CLK_LOCAL_MEM_FENCE_isSet(Flags1), CLK_LOCAL_MEM_FENCE_isSet(Flags2)));
- }
- else if (NonLocalState.getGlobalVariables().Contains(v))
- {
- EqualityCondition = Expr.And(EqualityCondition,
- Expr.And(CLK_GLOBAL_MEM_FENCE_isSet(Flags1), CLK_GLOBAL_MEM_FENCE_isSet(Flags2)));
- }
- }
-
- AssumeGuard = Expr.Imp(EqualityCondition, AssumeGuard);
-
return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new AssumeCmd(Token.NoToken, AssumeGuard) }), null, null);
}
@@ -2329,23 +2260,11 @@ namespace GPUVerify return ErrorCount;
}
- if(!CommandLineOptions.BarrierParameters && BarrierProcedure.InParams.Length != 0)
+ if (BarrierProcedure.InParams.Length != 0)
{
Error(BarrierProcedure, "Barrier procedure must not take any arguments");
}
- if (CommandLineOptions.BarrierParameters)
- {
- if (BarrierProcedure.InParams.Length != 1)
- {
- Error(BarrierProcedure, "Barrier procedure must take exactly one argument");
- }
- else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(32)))
- {
- Error(BarrierProcedure, "Argument to barrier procedure must have type bv32");
- }
- }
-
if (BarrierProcedure.OutParams.Length != 0)
{
Error(BarrierProcedure, "Barrier procedure must not return any results");
diff --git a/Test/VSComp2010/AnswerNoRuntimeChecking b/Test/VSComp2010/AnswerNoRuntimeChecking deleted file mode 100644 index d0492caf..00000000 --- a/Test/VSComp2010/AnswerNoRuntimeChecking +++ /dev/null @@ -1,15 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 858b6370..00000000 --- a/Test/VSComp2010/AnswerRuntimeChecking +++ /dev/null @@ -1,4 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 4efd244a..00000000 --- a/Test/VSComp2010/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,28 +0,0 @@ -@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 deleted file mode 100644 index d3b8a733..00000000 --- a/Test/VSComp2010/runtestRuntimeChecking.bat +++ /dev/null @@ -1,33 +0,0 @@ -@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 deleted file mode 100644 index 81ac67ef..00000000 --- a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking +++ /dev/null @@ -1,32 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 49a440db..00000000 --- a/Test/VSI-Benchmarks/AnswerRuntimeChecking +++ /dev/null @@ -1,21 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index c85b7606..00000000 --- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,27 +0,0 @@ -@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 deleted file mode 100644 index 27df70a3..00000000 --- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat +++ /dev/null @@ -1,33 +0,0 @@ -@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 deleted file mode 100644 index 04ece8ae..00000000 --- a/Test/dafny0/AnswerNoRuntimeChecking +++ /dev/null @@ -1,328 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index e3970b78..00000000 --- a/Test/dafny0/AnswerRuntimeChecking +++ /dev/null @@ -1,272 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index c90930d5..00000000 --- a/Test/dafny0/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,44 +0,0 @@ -@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 deleted file mode 100644 index 42d21010..00000000 --- a/Test/dafny0/runtestRuntimeChecking.bat +++ /dev/null @@ -1,55 +0,0 @@ -@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 deleted file mode 100644 index 5472ec14..00000000 --- a/Test/dafny1/AnswerNoRuntimeChecking +++ /dev/null @@ -1,76 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 1ade5aeb..00000000 --- a/Test/dafny1/AnswerRuntimeChecking +++ /dev/null @@ -1,27 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index a4989fa1..00000000 --- a/Test/dafny1/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,36 +0,0 @@ -@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 deleted file mode 100644 index fc32fbf4..00000000 --- a/Test/dafny1/runtestRuntimeChecking.bat +++ /dev/null @@ -1,51 +0,0 @@ -@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 deleted file mode 100644 index f04bb934..00000000 --- a/Test/dafny2/AnswerNoRuntimeChecking +++ /dev/null @@ -1,30 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 32b61bb1..00000000 --- a/Test/dafny2/AnswerRuntimeChecking +++ /dev/null @@ -1,7 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index b60fd69c..00000000 --- a/Test/dafny2/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,34 +0,0 @@ -@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 deleted file mode 100644 index 4ba447a7..00000000 --- a/Test/dafny2/runtestRuntimeChecking.bat +++ /dev/null @@ -1,39 +0,0 @@ -@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 deleted file mode 100644 index 11e295fc..00000000 --- a/Test/dafnyCompiler/Answer +++ /dev/null @@ -1,32 +0,0 @@ ------ 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 deleted file mode 100644 index 6b3abbd4..00000000 --- a/Test/dafnyCompiler/compilerTests.txt +++ /dev/null @@ -1,8 +0,0 @@ -..\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 deleted file mode 100644 index 0df12552..00000000 --- a/Test/dafnyCompiler/runtest.bat +++ /dev/null @@ -1,56 +0,0 @@ -@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 deleted file mode 100644 index a0446aa3..00000000 --- a/Test/dafnyCompiler/runtestall.bat +++ /dev/null @@ -1,10 +0,0 @@ -@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 deleted file mode 100644 index 0cc946ab..00000000 --- a/Test/dafnyRuntimeChecking/Answer +++ /dev/null @@ -1,4826 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 6fffd815..00000000 --- a/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking +++ /dev/null @@ -1,24 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 860dc843..00000000 --- a/Test/dafnyRuntimeChecking/AnswerRuntimeChecking +++ /dev/null @@ -1,32 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 5596e9e9..00000000 --- a/Test/dafnyRuntimeChecking/AssertStmt0.dfy +++ /dev/null @@ -1,4 +0,0 @@ -method Main()
-{
- assert 2 < 10;
-}
diff --git a/Test/dafnyRuntimeChecking/AssertStmt1.dfy b/Test/dafnyRuntimeChecking/AssertStmt1.dfy deleted file mode 100644 index 2730e87c..00000000 --- a/Test/dafnyRuntimeChecking/AssertStmt1.dfy +++ /dev/null @@ -1,4 +0,0 @@ -method Main()
-{
- assert 10 < 2;
-}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt0.dfy b/Test/dafnyRuntimeChecking/AssumeStmt0.dfy deleted file mode 100644 index 13f58deb..00000000 --- a/Test/dafnyRuntimeChecking/AssumeStmt0.dfy +++ /dev/null @@ -1,4 +0,0 @@ -method Main()
-{
- assume 2 < 10;
-}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt1.dfy b/Test/dafnyRuntimeChecking/AssumeStmt1.dfy deleted file mode 100644 index 7a749f51..00000000 --- a/Test/dafnyRuntimeChecking/AssumeStmt1.dfy +++ /dev/null @@ -1,4 +0,0 @@ -method Main()
-{
- assume 10 < 2;
-}
diff --git a/Test/dafnyRuntimeChecking/Postcondition0.dfy b/Test/dafnyRuntimeChecking/Postcondition0.dfy deleted file mode 100644 index 5b61988c..00000000 --- a/Test/dafnyRuntimeChecking/Postcondition0.dfy +++ /dev/null @@ -1,3 +0,0 @@ -method Main()
- ensures true;
-{}
diff --git a/Test/dafnyRuntimeChecking/Postcondition1.dfy b/Test/dafnyRuntimeChecking/Postcondition1.dfy deleted file mode 100644 index 0969c51d..00000000 --- a/Test/dafnyRuntimeChecking/Postcondition1.dfy +++ /dev/null @@ -1,11 +0,0 @@ -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 deleted file mode 100644 index 73733bbb..00000000 --- a/Test/dafnyRuntimeChecking/Precondition0.dfy +++ /dev/null @@ -1,3 +0,0 @@ -method Main()
- requires true;
-{}
diff --git a/Test/dafnyRuntimeChecking/Precondition1.dfy b/Test/dafnyRuntimeChecking/Precondition1.dfy deleted file mode 100644 index 1732b0bc..00000000 --- a/Test/dafnyRuntimeChecking/Precondition1.dfy +++ /dev/null @@ -1,9 +0,0 @@ -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 deleted file mode 100644 index 3e434f49..00000000 --- a/Test/dafnyRuntimeChecking/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@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 deleted file mode 100644 index e336e022..00000000 --- a/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,25 +0,0 @@ -@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 deleted file mode 100644 index 6b086f6f..00000000 --- a/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat +++ /dev/null @@ -1,25 +0,0 @@ -@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 ca40465e..2b457c91 100644 --- a/Test/dafnytests.txt +++ b/Test/dafnytests.txt @@ -1,9 +1,7 @@ -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
+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
diff --git a/Test/runtest.bat b/Test/runtest.bat index 8a75f363..5b3d45ae 100644 --- a/Test/runtest.bat +++ b/Test/runtest.bat @@ -5,12 +5,7 @@ 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 deleted file mode 100644 index a1f7f57b..00000000 --- a/Test/vacid0/AnswerNoRuntimeChecking +++ /dev/null @@ -1,9 +0,0 @@ -
--------------------- LazyInitArray --------------------
-Compiled assembly into LazyInitArray.dll
-
--------------------- SparseArray --------------------
-Compiled assembly into SparseArray.dll
-
--------------------- Composite --------------------
-Compiled assembly into Composite.exe
diff --git a/Test/vacid0/runtestNoRuntimeChecking.bat b/Test/vacid0/runtestNoRuntimeChecking.bat deleted file mode 100644 index 3a7befa2..00000000 --- a/Test/vacid0/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,27 +0,0 @@ -@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 deleted file mode 100644 index 077c1002..00000000 --- a/Test/vacid0/runtestRuntimeChecking.bat +++ /dev/null @@ -1,32 +0,0 @@ -@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 deleted file mode 100644 index c5508749..00000000 --- a/Test/vstte2012/AnswerNoRuntimeChecking +++ /dev/null @@ -1,18 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 5c703cc7..00000000 --- a/Test/vstte2012/AnswerRuntimeChecking +++ /dev/null @@ -1,11 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index e572ed2f..00000000 --- a/Test/vstte2012/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,28 +0,0 @@ -@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 deleted file mode 100644 index 042efe96..00000000 --- a/Test/vstte2012/runtestRuntimeChecking.bat +++ /dev/null @@ -1,32 +0,0 @@ -@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
- )
-)
|