diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index a800e288fb0..cb6737b4a81 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,7 @@ # Upcoming - fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854) +- fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833) # 3.9.0 @@ -8,6 +9,7 @@ - feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717) - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq)` (https://github.com/dafny-lang/dafny/pull/2594) - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610) +- feat: Support arbitrary version of z3 for the language server. Dafny is still distributed with z3 4.8.5 and uses that version by default. (https://github.com/dafny-lang/dafny/pull/2820) - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658) - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668) - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716) diff --git a/Source/DafnyCore/AST/Types.cs b/Source/DafnyCore/AST/Types.cs index 314b162c24a..50deb663849 100644 --- a/Source/DafnyCore/AST/Types.cs +++ b/Source/DafnyCore/AST/Types.cs @@ -2018,7 +2018,11 @@ public static string PrettyArrowTypeName(string arrow, List typeArgs, Type s += Util.Comma(typeArgs.Take(arity), arg => arg.TypeName(context, parseAble)); if (domainNeedsParens) { s += ")"; } s += " " + arrow + " "; - s += (result ?? typeArgs.Last()).TypeName(context, parseAble); + if (result != null || typeArgs.Count >= 1) { + s += (result ?? typeArgs.Last()).TypeName(context, parseAble); + } else { + s += ""; + } return s; } diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index f020e5e9cc7..53c1603ff60 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1,4 +1,5 @@ -/*----------------------------------------------------------------------------- +/* ( +----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // Copyright by the contributors to the Dafny Project @@ -96,7 +97,11 @@ void CheckDeclModifiers(ref DeclModifierData dmod, string declCaption, AllowedDe } if (dmod.IsGhost) { if ((allowed & AllowedDeclModifiers.AlreadyGhost) != 0) { - SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost' (it is 'ghost' by default)"); + if (declCaption.Contains("-by-method")) { + SemErr(dmod.GhostToken, $"{declCaption} has a ghost function body and a non-ghost method body; {declCaption} declaration does not use the 'ghost' keyword."); + } else { + SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost' (it is 'ghost' by default)"); + } dmod.IsGhost = false; } else if ((allowed & AllowedDeclModifiers.Ghost) == 0) { SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost'"); diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 2ec901893b1..3a02032bc4e 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -1239,8 +1239,9 @@ focal predicate P to P#[_k-1]. /extractCounterexample If verification fails, report a detailed counterexample for the - first failing assertion. Requires specifying the /mv option as well - as /proverOpt:O:model_compress=false and + first failing assertion. Requires specifying the /mv: option as well + as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or + /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and /proverOpt:O:model.completion=true. /countVerificationErrors: diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index f6e86976bcd..1514726791c 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -873,7 +873,10 @@ public IEnumerable GetExpansion(DafnyModelState state, Dafny return result; } - private const string PleaseEnableModelCompressFalse = "Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values."; + private const string PleaseEnableModelCompressFalse = + "Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7)" + + " or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7)," + + " otherwise you'll get unexpected values."; /// /// Return the name of the field represented by the given element. diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 8ae4e3eb8c8..425c2bf1026 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics; +using System.Text.RegularExpressions; using Microsoft.Dafny.LanguageServer.Handlers; using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Workspace; @@ -14,7 +15,7 @@ using System.Threading.Tasks; using Microsoft.Boogie.SMTLib; using Microsoft.Extensions.Options; -using OmniSharp.Extensions.LanguageServer.Protocol.Window; +using Action = System.Action; namespace Microsoft.Dafny.LanguageServer { public static class DafnyLanguageServer { @@ -55,6 +56,8 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req return Task.CompletedTask; } + private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?\d+)\.(?\d+)\.(?\d+)"); + private static void PublishSolverPath(ILanguageServer server) { var telemetryPublisher = server.GetRequiredService(); string solverPath; @@ -62,6 +65,7 @@ private static void PublishSolverPath(ILanguageServer server) { var proverOptions = new SMTLibSolverOptions(DafnyOptions.O); proverOptions.Parse(DafnyOptions.O.ProverOptions); solverPath = proverOptions.ExecutablePath(); + HandleZ3Version(telemetryPublisher, proverOptions); } catch (Exception e) { solverPath = $"Error while determining solver path: {e}"; } @@ -69,6 +73,44 @@ private static void PublishSolverPath(ILanguageServer server) { telemetryPublisher.PublishSolverPath(solverPath); } + private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) { + var z3Process = new ProcessStartInfo(proverOptions.ProverPath, "-version") { + CreateNoWindow = true, + RedirectStandardError = true, + RedirectStandardOutput = true, + RedirectStandardInput = true + }; + var run = Process.Start(z3Process); + if (run == null) { + return; + } + + var actualOutput = run.StandardOutput.ReadToEnd(); + run.WaitForExit(); + var versionMatch = Z3VersionRegex.Match(actualOutput); + if (!versionMatch.Success) { + // Might be another solver. + return; + } + + telemetryPublisher.PublishZ3Version(versionMatch.Value); + var major = int.Parse(versionMatch.Groups["major"].Value); + var minor = int.Parse(versionMatch.Groups["minor"].Value); + var patch = int.Parse(versionMatch.Groups["patch"].Value); + if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) { + return; + } + + var toReplace = "O:model_compress=false"; + var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace); + if (i == -1) { + telemetryPublisher.PublishUnhandledException(new Exception($"Z3 version is > 4.8.6 but I did not find {toReplace} in the prover options:" + string.Join(" ", DafnyOptions.O.ProverOptions))); + return; + } + + DafnyOptions.O.ProverOptions[i] = "O:model.compact=false"; + } + /// /// Load the plugins for the Dafny pipeline /// diff --git a/Source/DafnyLanguageServer/Workspace/DocumentOptions.cs b/Source/DafnyLanguageServer/Workspace/DocumentOptions.cs index e78428624bb..e9d44e84e30 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentOptions.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentOptions.cs @@ -28,7 +28,7 @@ static DocumentOptions() { public List AugmentedProverOptions => DafnyOptions.O.ProverOptions.Concat(new List() { - "O:model_compress=false", + "O:model_compress=false", // Replaced by "O:model.compact=false" if z3's version is > 4.8.6 "O:model.completion=true", "O:model_evaluator.completion=true" }).ToList(); diff --git a/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs b/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs index 2553d89a776..fac20b59671 100644 --- a/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs @@ -12,7 +12,8 @@ public interface ITelemetryPublisher { protected enum TelemetryEventKind { UpdateComplete, UnhandledException, - SolverPath + SolverPath, + Z3Version } /// @@ -37,5 +38,9 @@ public void PublishUpdateComplete() { public void PublishSolverPath(string solverPath) { PublishTelemetry(TelemetryEventKind.SolverPath, solverPath); } + + public void PublishZ3Version(string z3Version) { + PublishTelemetry(TelemetryEventKind.Z3Version, z3Version); + } } } \ No newline at end of file diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect index 59331db20d8..cca24ccbaa2 100644 --- a/Test/dafny0/ParseErrors.dfy.expect +++ b/Test/dafny0/ParseErrors.dfy.expect @@ -56,15 +56,15 @@ ParseErrors.dfy(220,2): Error: a module cannot be declared 'static' ParseErrors.dfy(226,2): Error: a datatype or codatatype cannot be declared 'ghost' ParseErrors.dfy(227,2): Error: a module cannot be declared 'ghost' ParseErrors.dfy(234,51): Error: a 'by method' implementation is not allowed on a twostate function -ParseErrors.dfy(234,2): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +ParseErrors.dfy(234,2): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. ParseErrors.dfy(235,52): Error: a 'by method' implementation is not allowed on a twostate function ParseErrors.dfy(236,50): Error: a 'by method' implementation is not allowed on a twostate predicate -ParseErrors.dfy(236,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +ParseErrors.dfy(236,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. ParseErrors.dfy(237,51): Error: a 'by method' implementation is not allowed on a twostate predicate ParseErrors.dfy(240,47): Error: a 'by method' implementation is not allowed on an extreme predicate -ParseErrors.dfy(240,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +ParseErrors.dfy(240,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. ParseErrors.dfy(241,50): Error: a 'by method' implementation is not allowed on an extreme predicate -ParseErrors.dfy(241,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +ParseErrors.dfy(241,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. ParseErrors.dfy(244,55): Error: a 'by method' implementation is not allowed on a twostate function ParseErrors.dfy(244,2): Error: a function-by-method cannot be declared 'abstract' ParseErrors.dfy(245,54): Error: a 'by method' implementation is not allowed on a twostate predicate diff --git a/Test/git-issues/git-issue-1564.dfy.expect b/Test/git-issues/git-issue-1564.dfy.expect index 8d4cba4f8b0..674d3932fd1 100644 --- a/Test/git-issues/git-issue-1564.dfy.expect +++ b/Test/git-issues/git-issue-1564.dfy.expect @@ -5,9 +5,9 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(42,0): Error: a predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(43,0): Error: a predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(46,19): Error: a twostate predicate is supported only as ghost, not as a compiled predicate @@ -15,9 +15,9 @@ git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 20 parse errors detected in git-issue-1564.dfy git-issue-1564.dfy(9,0): Error: a function must be declared as either 'ghost function' or 'function method' git-issue-1564.dfy(12,28): Error: there is no such thing as a 'ghost function method' @@ -26,9 +26,9 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(40,0): Error: a predicate must be declared as either 'ghost predicate' or 'predicate method' git-issue-1564.dfy(43,26): Error: there is no such thing as a 'ghost predicate method' git-issue-1564.dfy(46,19): Error: a twostate predicate is supported only as ghost, not as a compiled predicate @@ -36,9 +36,9 @@ git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 20 parse errors detected in git-issue-1564.dfy git-issue-1564.dfy(10,22): Error: the phrase 'function method' is not allowed; to declare a compiled function, use just 'function' git-issue-1564.dfy(12,28): Error: the phrase 'function method' is not allowed; to declare a compiled function, use just 'function' @@ -47,9 +47,9 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(41,20): Error: the phrase 'predicate method' is not allowed; to declare a compiled predicate, use just 'predicate' git-issue-1564.dfy(43,26): Error: the phrase 'predicate method' is not allowed; to declare a compiled predicate, use just 'predicate' git-issue-1564.dfy(46,19): Error: a twostate predicate is supported only as ghost, not as a compiled predicate @@ -57,9 +57,9 @@ git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 20 parse errors detected in git-issue-1564.dfy git-issue-1564.dfy(12,28): Error: there is no such thing as a 'ghost function method' git-issue-1564.dfy(15,18): Error: a twostate function is supported only as ghost, not as a compiled function @@ -67,18 +67,18 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(43,26): Error: there is no such thing as a 'ghost predicate method' git-issue-1564.dfy(46,19): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 18 parse errors detected in git-issue-1564.dfy git-issue-1564.dfy(12,28): Error: there is no such thing as a 'ghost function method' git-issue-1564.dfy(15,18): Error: a twostate function is supported only as ghost, not as a compiled function @@ -86,18 +86,18 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(43,26): Error: there is no such thing as a 'ghost predicate method' git-issue-1564.dfy(46,19): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 18 parse errors detected in git-issue-1564.dfy git-issue-1564.dfy(10,22): Error: the phrase 'function method' is not allowed; to declare a compiled function, use just 'function' git-issue-1564.dfy(12,28): Error: the phrase 'function method' is not allowed; to declare a compiled function, use just 'function' @@ -106,9 +106,9 @@ git-issue-1564.dfy(16,0): Error: a twostate function cannot be declared 'ghost' git-issue-1564.dfy(17,24): Error: a twostate function is supported only as ghost, not as a compiled function git-issue-1564.dfy(17,0): Error: a twostate function cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(24,9): Error: to use a 'by method' implementation with a function, declare 'H1' using 'function', not 'function method' -git-issue-1564.dfy(29,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(29,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(34,15): Error: to use a 'by method' implementation with a function, declare 'H3' using 'function', not 'function method' -git-issue-1564.dfy(34,0): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(34,0): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(41,20): Error: a predicate is always ghost and is declared with 'predicate' git-issue-1564.dfy(42,0): Error: a predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(43,26): Error: a predicate is always ghost and is declared with 'predicate' @@ -117,7 +117,7 @@ git-issue-1564.dfy(47,0): Error: a twostate predicate cannot be declared 'ghost' git-issue-1564.dfy(48,25): Error: a twostate predicate is supported only as ghost, not as a compiled predicate git-issue-1564.dfy(48,0): Error: a twostate predicate cannot be declared 'ghost' (it is 'ghost' by default) git-issue-1564.dfy(55,10): Error: to use a 'by method' implementation with a predicate, declare 'R1' using 'predicate', not 'predicate method' -git-issue-1564.dfy(60,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(60,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. git-issue-1564.dfy(65,16): Error: to use a 'by method' implementation with a predicate, declare 'R3' using 'predicate', not 'predicate method' -git-issue-1564.dfy(65,0): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default) +git-issue-1564.dfy(65,0): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword. 21 parse errors detected in git-issue-1564.dfy diff --git a/Test/git-issues/git-issue-2026.dfy.expect b/Test/git-issues/git-issue-2026.dfy.expect index e0c27f25cff..68a7f79fc01 100644 --- a/Test/git-issues/git-issue-2026.dfy.expect +++ b/Test/git-issues/git-issue-2026.dfy.expect @@ -9,12 +9,12 @@ git-issue-2026.dfy(5,0): initial state: n : int = 5854 ret : ? = () git-issue-2026.dfy(6,24): -Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values. +Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), otherwise you'll get unexpected values. n : int = 5854 ret : ? = ([null] := @0) @0 : ? = () git-issue-2026.dfy(8,14): -Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values. +Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), otherwise you'll get unexpected values. n : int = 5854 ret : ? = ([null] := @0) i : int = 0 @@ -24,13 +24,13 @@ git-issue-2026.dfy(9,4): after some loop iterations: ret : ? = () i : int = 0 git-issue-2026.dfy(15,27): -Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values. +Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), otherwise you'll get unexpected values. n : int = 5854 ret : ? = ([null] := @0) i : int = 0 @0 : ? = () git-issue-2026.dfy(19,18): -Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values. +Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), otherwise you'll get unexpected values. n : int = 5854 ret : ? = ([null] := @0) i : int = 1 diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 7fed367c679..73644e1030e 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -17,9 +17,9 @@ in order of increasing binding power. `||`, `|` | 3 | disjunction (or) --------------------------|------------------------------------ `==` | 4 | equality - `==#[k]` | 4 | prefix equality (co-inductive) + `==#[k]` | 4 | prefix equality (coinductive) `!=` | 4 | disequality - `!=#[k]` | 4 | prefix disequality (co-inductive) + `!=#[k]` | 4 | prefix disequality (coinductive) `<` | 4 | less than `<=` | 4 | at most `>=` | 4 | at least @@ -203,7 +203,7 @@ The `!!` represents disjointness for sets and multisets as explained in [Section 10.1](#sec-sets) and [Section 10.2](#sec-multisets). Note that `x ==#[k] y` is the prefix equality operator that compares -co-inductive values for equality to a nesting level of k, as +coinductive values for equality to a nesting level of k, as explained in [the section about co-equality](#sec-co-equality). ## 21.6. Bit Shifts @@ -1038,7 +1038,7 @@ CaseExpression(allowLemma, allowLambda) = A ``MatchExpression`` is used to conditionally evaluate and select an expression depending on the value of an algebraic type, i.e. an inductive -type, a co-inductive type, or a base type. +type, a coinductive type, or a base type. The ``Expression`` following the `match` keyword is called the _selector_. The selector is evaluated and then matched against each ``CaseExpression`` in order until a matching clause is found, as described in @@ -1389,7 +1389,7 @@ greatest lemma {:induction false} Theorem0(s: T) ensures atmost(zeros(s), ones(s)) { // the following shows two equivalent ways to state the - // co-inductive hypothesis + // coinductive hypothesis if (*) { Theorem0#[_k-1](s); } else { diff --git a/docs/DafnyRef/Introduction.md b/docs/DafnyRef/Introduction.md index 12bbf492f2f..2e796744ae7 100644 --- a/docs/DafnyRef/Introduction.md +++ b/docs/DafnyRef/Introduction.md @@ -12,7 +12,7 @@ executable form. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, inheritance and abstraction, methods and functions, dynamic allocation, inductive and -co-inductive datatypes, and specification constructs. The +coinductive datatypes, and specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 7e158485035..48cd2b8c292 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -344,8 +344,9 @@ Usage: Dafny [ option ... ] [ filename ... ] /extractCounterexample If verification fails, report a detailed counterexample for the - first failing assertion. Requires specifying the /mv option as well - as /proverOpt:O:model_compress=false and + first failing assertion. Requires specifying the /mv: option as well + as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or + /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and /proverOpt:O:model.completion=true. /countVerificationErrors: diff --git a/docs/DafnyRef/Programs.md b/docs/DafnyRef/Programs.md index f7f632620f4..35daaffa381 100644 --- a/docs/DafnyRef/Programs.md +++ b/docs/DafnyRef/Programs.md @@ -5,7 +5,7 @@ Dafny = { IncludeDirective_ } { TopDecl } EOF At the top level, a Dafny program (stored as files with extension `.dfy`) is a set of declarations. The declarations introduce (module-level) constants, methods, functions, lemmas, types (classes, traits, inductive and -co-inductive datatypes, newtypes, type synonyms, opaque types, and +coinductive datatypes, newtypes, type synonyms, opaque types, and iterators) and modules, where the order of introduction is irrelevant. A class also contains a set of declarations, introducing fields, methods, and functions. diff --git a/docs/DafnyRef/README.md b/docs/DafnyRef/README.md index ade1db59a90..f001dfdb90a 100644 --- a/docs/DafnyRef/README.md +++ b/docs/DafnyRef/README.md @@ -24,11 +24,11 @@ other aspects that are dissimilar between the pdf and online versions. GitHub pages are rendered (converted from markdown to html) using Jekyll. The result is a single, long html page. -There are a number of configuration files for Jekyll in the docs folder and +There are a number of configuration files for Jekyll in the `docs` folder and subfolders. In order to render files locally you must -* have ruby, bundler and jekyll installed on your machine -* set the working directly (cd) to the docs folder (Windows or Ruby 3.0 users, see below for some tweaks) -* run the jekyll server: bundle exec jekyll server +* have `ruby`, `bundler` and `jekyll` installed on your machine +* set the working directly (`cd`) to the `docs` folder (Windows or Ruby 3.0 users, see below for some tweaks) +* run the jekyll server: `bundle exec jekyll server` * open a browser on the page http://localhost:4000 or directly to http://localhost:4000/DafnyRef/DafnyRef * the server rerenders when files are changed -- but not always quite completely. Sometimes one must kill the server process, delete all the files in the _saite folder, and restart the server. @@ -38,6 +38,8 @@ The Makefile does some preprocessing of the markdown files: it removes some markdown lines that are not interpreted by pandoc and adds some additional directives, such as page breaks. +To re-generate `Options.txt`, run `make options` in the `DafnyRef` folder. + ## Windows users or Ruby 3.0 users You might want to apply this diff to the file `../GemFile` @@ -111,4 +113,4 @@ file as well. ## LSP Many IDEs interact with Language Servers (via LSP). Possibly an LSP protocol -will be generated in the future. +will be generated in the future. \ No newline at end of file diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md index 122d08ec6ce..42d2b912337 100644 --- a/docs/DafnyRef/Statements.md +++ b/docs/DafnyRef/Statements.md @@ -1469,7 +1469,7 @@ CaseStmt = "case" ExtendedPattern "=>" { Stmt } [ `ExtendedPattern` is defined in [Section 21.33](#sec-case-pattern).] -The `match` statement is used to do case analysis on a value of an inductive or co-inductive datatype (which includes the built-in tuple types), a base type, or newtype. The expression after the `match` keyword is called the _selector_. The expression is evaluated and then matched against +The `match` statement is used to do case analysis on a value of an inductive or coinductive datatype (which includes the built-in tuple types), a base type, or newtype. The expression after the `match` keyword is called the _selector_. The expression is evaluated and then matched against each clause in order until a matching clause is found. The process of matching the selector expression against the `CaseBinding_`s is @@ -1924,7 +1924,7 @@ forall x :: P(x) ==> Q(x). ``` The `forall` statement is also used extensively in the de-sugared forms of -co-predicates and co-lemmas. See [datatypes](#sec-co-inductive-datatypes). +co-predicates and co-lemmas. See [datatypes](#sec-coinductive-datatypes). ## 20.22. Modify Statement {#sec-modify-statement} ````grammar diff --git a/docs/DafnyRef/Topics.md b/docs/DafnyRef/Topics.md index 24115e987de..07574503914 100644 --- a/docs/DafnyRef/Topics.md +++ b/docs/DafnyRef/Topics.md @@ -276,7 +276,7 @@ encoding makes it possible to reason about fixpoints in an automated way. The encoding for greatest predicates in Dafny was described previously -[@LeinoMoskal:Coinduction] and is here described in [the section about datatypes](#sec-co-inductive-datatypes). +[@LeinoMoskal:Coinduction] and is here described in [the section about datatypes](#sec-coinductive-datatypes). ### 24.4.1. Function Definitions @@ -1030,7 +1030,7 @@ are given in the following table: | `map` | `x.Keys` is a proper subset of `X.Keys` | | inductive datatypes | `x` is structurally included in `X` | | reference types | `x == null && X != null` | -| co-inductive datatypes | `false` | +| coinductive datatypes | `false` | | type parameter | `false` | | arrow types | `false` | diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 73ca648289d..df9a930a211 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -33,7 +33,7 @@ These are: * The basic scalar types: `bool`, `char`, `int`, `real`, `ORDINAL`, bitvector types * The built-in collection types: `set`, `iset`, `multiset`, `seq`, `string`, `map`, `imap` * Tuple Types -* Inductive and co-inductive types +* Inductive and coinductive types * Function (arrow) types * Subset and newtypes that are based on value types @@ -61,7 +61,7 @@ NamedType = NameSegmentForTypeName { "." NameSegmentForTypeName } A ``NamedType`` is used to specify a user-defined type by name (possibly module-qualified). Named types are introduced by -class, trait, inductive, co-inductive, synonym and opaque +class, trait, inductive, coinductive, synonym and opaque type declarations. They are also used to refer to type variables. ````grammar @@ -570,7 +570,7 @@ is a method whose type parameter is restricted to equality-supporting types when used in a non-ghost context. Again, note that _all_ types support equality in _ghost_ contexts; the difference is only for non-ghost (that is, compiled) -code. Co-inductive datatypes, arrow types, and inductive +code. Coinductive datatypes, arrow types, and inductive datatypes with ghost parameters are examples of types that are not equality supporting. @@ -2374,10 +2374,9 @@ function Fib(n: nat): nat { } ``` -The `by method` clause is allowed only for the `function` or `predicate` -declarations (without `method`, `twostate`, `least`, and `greatest`, but -possibly with `static`). The method -inherits the in-parameters, attributes, and `requires` and `decreases` +The `by method` clause is allowed only for non-ghost `function` or `predicate` +declarations (without `twostate`, `least`, and `greatest`, but +possibly with `static`); it inherits the in-parameters, attributes, and `requires` and `decreases` clauses of the function. The method also gets one out-parameter, corresponding to the function's result value (and the name of it, if present). Finally, the method gets an empty `modifies` clause and a postcondition @@ -2463,9 +2462,12 @@ function Factorial(n: int): (f: int) } ``` -By default, a function is `ghost`, and cannot be called from non-ghost +Pre v4.0, a function is `ghost` by default, and cannot be called from non-ghost code. To make it non-ghost, replace the keyword `function` with the two -keywords "`function method`". [TODO: This use of keywords is proposed to change.] +keywords "`function method`". From v4.0 on, a function is non-ghost by +default. To make it ghost, replace the keyword `function` with the two keywords "`ghost function`". +(See the [/functionSyntax option](#sec-function-syntax) for a description +of the migration path for this change in behavior.} Like methods, functions can be either _instance_ (which they are by default) or _static_ (when the function declaration contains the keyword `static`). @@ -3596,7 +3598,7 @@ DatatypeMemberDecl = ```` Dafny offers two kinds of algebraic datatypes, those defined -inductively (with `datatype`) and those defined co-inductively (with `codatatype`). +inductively (with `datatype`) and those defined coinductively (with `codatatype`). The salient property of every datatype is that each value of the type uniquely identifies one of the datatype's constructors and each constructor is injective in @@ -3606,7 +3608,7 @@ its parameters. The values of inductive datatypes can be seen as finite trees where the leaves are values of basic types, numeric types, reference types, -co-inductive datatypes, or arrow types. Indeed, values of +coinductive datatypes, or arrow types. Indeed, values of inductive datatypes can be compared using Dafny's well-founded `<` ordering. @@ -3718,17 +3720,13 @@ Note that only `<` is defined; not `<=` or `>` or `>=`. Also, `<` is underspecified. With the above code, one can prove neither `z < x` nor `!(z < x)` and neither `z < y` nor `!(z < y)`. In each pair, though, one or the other is true, so `(z < x) || !(z < x)` is provable. -## 19.2. Co-inductive datatypes {#sec-co-inductive-datatypes} - -TODO: This section and particularly the subsections need rewriting using -the least and greatest terminology, and to make the text fit better into -the overall reference manual. +## 19.2. Coinductive datatypes {#sec-coinductive-datatypes} Whereas Dafny insists that there is a way to construct every inductive datatype value from the ground up, Dafny also supports -_co-inductive datatypes_, whose constructors are evaluated lazily, and +_coinductive datatypes_, whose constructors are evaluated lazily, and hence the language allows infinite structures. -A co-inductive datatype is declared +A coinductive datatype is declared using the keyword `codatatype`; other than that, it is declared and used like an inductive datatype. @@ -3743,14 +3741,14 @@ finite or infinite), infinite streams (that is, lists that are always infinite), and infinite binary trees (that is, trees where every branch goes on forever), respectively. -The paper [Co-induction Simply], by Leino and +The paper [Co-induction Simply](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/coinduction.pdf), by Leino and Moskal[@LEINO:Dafny:Coinduction], explains Dafny's implementation and -verification of co-inductive types. We capture the key features from that +verification of coinductive types. We capture the key features from that paper in this section but the reader is referred to that paper for more complete details and to supply bibliographic references that are omitted here. -## 19.3. Co-induction {#sec-coinduction} +## 19.3. Coinduction {#sec-coinduction} Mathematical induction is a cornerstone of programming and program verification. It arises in data definitions (e.g., some algebraic data @@ -3758,25 +3756,25 @@ structures can be described using induction), it underlies program semantics (e.g., it explains how to reason about finite iteration and recursion), and it is used in proofs (e.g., supporting lemmas about data structures use inductive proofs). Whereas induction deals with -finite things (data, behavior, etc.), its dual, co-induction, deals with -possibly infinite things. Co-induction, too, is important in programming +finite things (data, behavior, etc.), its dual, coinduction, deals with +possibly infinite things. Coinduction, too, is important in programming and program verification: it arises in data definitions (e.g., lazy data structures), semantics (e.g., concurrency), and proofs (e.g., -showing refinement in a co-inductive big-step semantics). It is thus -desirable to have good support for both induction and co-induction in a +showing refinement in a coinductive big-step semantics). It is thus +desirable to have good support for both induction and coinduction in a system for constructing and reasoning about programs. Co-datatypes and co-recursive functions make it possible to use lazily -evaluated data structures (like in Haskell or Agda). Co-predicates, +evaluated data structures (like in Haskell or Agda). _Greatest predicates_, defined by greatest fix-points, let programs state properties of such data structures (as can also be done in, for example, Coq). For the -purpose of writing co-inductive proofs in the language, we introduce -co-lemmas. Ostensibly, a co-lemma invokes the co-induction hypothesis +purpose of writing coinductive proofs in the language, we introduce +greatest and least lemmas. A greatest lemma invokes the coinduction hypothesis much like an inductive proof invokes the induction hypothesis. Underneath -the hood, our co-inductive proofs are actually approached via induction: -co-lemmas provide a syntactic veneer around this approach. +the hood, our coinductive proofs are actually approached via induction: +greatest and least lemmas provide a syntactic veneer around this approach. -The following example gives a taste of how the co-inductive features in +The following example gives a taste of how the coinductive features in Dafny come together to give straightforward definitions of infinite matters. ```dafny @@ -3813,13 +3811,13 @@ greatest lemma NotATheorem_SquareBelow(a: IStream) The example defines a type `IStream` of infinite streams, with constructor `ICons` and destructors `head` and `tail`. Function `Mult` performs pointwise multiplication on infinite streams of integers, defined using a -co-recursive call (which is evaluated lazily). Co-predicate `Below` is +co-recursive call (which is evaluated lazily). Greatest predicate `Below` is defined as a greatest fix-point, which intuitively means that the co-predicate will take on the value true if the recursion goes on forever -without determining a different value. The co-lemma states the theorem +without determining a different value. The greatest lemma states the theorem `Below(a, Mult(a, a))`. Its body gives the proof, where the recursive invocation of the co-lemma corresponds to an invocation of the -co-induction hypothesis. +coinduction hypothesis. The proof of the theorem stated by the first co-lemma lends itself to the following intuitive reading: To prove that `a` is below @@ -3829,27 +3827,27 @@ a property that does not always hold; the verifier is not fooled by the bogus proof attempt and instead reports the property as unproved. We argue that these definitions in Dafny are simple enough to level the -playing field between induction (which is familiar) and co-induction +playing field between induction (which is familiar) and coinduction (which, despite being the dual of induction, is often perceived as eerily mysterious). Moreover, the automation provided by our SMT-based verifier -reduces the tedium in writing co-inductive proofs. For example, it -verifies `Theorem_BelowSquare` from the program text given above— no +reduces the tedium in writing coinductive proofs. For example, it +verifies `Theorem_BelowSquare` from the program text given above---no additional lemmas or tactics are needed. In fact, as a consequence of the automatic-induction heuristic in Dafny, the verifier will automatically verify `Theorem_BelowSquare` even given an empty body. Just like there are restrictions on when an _inductive hypothesis_ can be -invoked, there are restrictions on how a _co-inductive_ hypothesis can be +invoked, there are restrictions on how a _coinductive_ hypothesis can be _used_. These are, of course, taken into consideration by Dafny's verifier. -For example, as illustrated by the second co-lemma above, invoking the -co-inductive hypothesis in an attempt to obtain the entire proof goal is +For example, as illustrated by the second greatest lemma above, invoking the +coinductive hypothesis in an attempt to obtain the entire proof goal is futile. (We explain how this works in [the section about greatest lemmas](#sec-colemmas)) Our initial experience -with co-induction in Dafny shows it to provide an intuitive, low-overhead +with coinduction in Dafny shows it to provide an intuitive, low-overhead user experience that compares favorably to even the best of today’s -interactive proof assistants for co-induction. In addition, the -co-inductive features and verification support in Dafny have other +interactive proof assistants for coinduction. In addition, the +coinductive features and verification support in Dafny have other potential benefits. The features are a stepping stone for verifying -functional lazy programs with Dafny. Co-inductive features have also +functional lazy programs with Dafny. Coinductive features have also shown to be useful in defining language semantics, as needed to verify the correctness of a compiler, so this opens the possibility that such verifications can benefit from SMT automation. @@ -3893,10 +3891,10 @@ is used to invoke `Lemma(x)` on all `x` for which `P(x)` holds. If forall x :: P(x) ==> Q(x). ``` -### 19.3.2. Defining Co-inductive Datatypes +### 19.3.2. Defining Coinductive Datatypes Each value of an inductive datatype is finite, in the sense that it can be constructed by a finite number of calls to datatype constructors. In -contrast, values of a co-inductive datatype, or co-datatype for short, +contrast, values of a coinductive datatype, or co-datatype for short, can be infinite. For example, a co-datatype can be used to represent infinite trees. @@ -3918,7 +3916,7 @@ function FivesUp(n: int): Stream } ``` -`Stream` is a co-inductive datatype whose values are possibly infinite +`Stream` is a coinductive datatype whose values are possibly infinite lists. Function `Up` returns a stream consisting of all integers upwards of `n` and `FivesUp` returns a stream consisting of all multiples of 5 upwards of `n` . The self-call in `Up` and the first self-call in `FivesUp` @@ -3928,7 +3926,7 @@ not in a productive position and is therefore subject to termination checking; in particular, each recursive call must decrease the rank defined by the `decreases` clause. -Analogous to the common finite list datatype, Stream declares two +Analogous to the common finite list datatype, `Stream` declares two constructors, `SNil` and `SCons`. Values can be destructed using match expressions and statements. In addition, like for inductive datatypes, each constructor `C` automatically gives rise to a discriminator `C?` and @@ -3992,7 +3990,7 @@ greatest predicate Pos(s: Stream) // Automatically generated by the Dafny compiler: predicate Pos#[_k: nat](s: Stream) decreases _k -{ if _k = 0 then true else +{ if _k == 0 then true else match s case SNil => true case SCons(x, rest) => x > 0 && Pos#[_k-1](rest) @@ -4000,21 +3998,24 @@ predicate Pos#[_k: nat](s: Stream) ``` Some restrictions apply. To guarantee that the greatest fix-point always -exists, the (implicit functor defining the) co-predicate must be +exists, the (implicit functor defining the) greatest predicate must be monotonic. This is enforced by a syntactic restriction on the form of the -body of co-predicates: after conversion to negation normal form (i.e., +body of greatest predicates: after conversion to negation normal form (i.e., pushing negations down to the atoms), intra-cluster calls of -co-predicates must appear only in _positive_ positions—that is, they must +greatest predicates must appear only in _positive_ positions—that is, they must appear as atoms and must not be negated. Additionally, to guarantee -soundness later on, we require that they appear in _co-friendly_ +soundness later on, we require that they appear in _continous_ positions—that is, in negation normal form, when they appear under existential quantification, the quantification needs to be limited to a -finite range[^fn-copredicate-restriction]. Since the evaluation of a co-predicate might not -terminate, co-predicates are always ghost. There is also a restriction on -the call graph that a cluster containing a co-predicate must contain only -co-predicates, no other kinds of functions. - -[^fn-copredicate-restriction]: Higher-order function support in Dafny is +finite range[^fn-copredicate-restriction]. Since the evaluation of a greatest predicate might not +terminate, greatest predicates are always ghost. There is also a restriction on +the call graph that a cluster containing a greatest predicate must contain only +greatest predicates, no other kinds of functions. + +[^fn-copredicate-restriction]: To be specific, Dafny has two forms of +extreme predicates and lemmas, one in which `_k` has type `nat` and one in +which it has type `ORDINAL` (the default). The continuous restriction +applies only when `_k` is `nat`. Also, higher-order function support in Dafny is rather modest and typical reasoning patterns do not involve them, so this restriction is not as limiting as it would have been in, e.g., Coq. @@ -4026,15 +4027,15 @@ from the co-predicate by * adding a parameter `_k` of type `nat` to denote the prefix length, * adding the clause `decreases _k;` to the prefix predicate (the - co-predicate itself is not allowed to have a decreases clause), + greatest predicate itself is not allowed to have a decreases clause), -* replacing in the body of the co-predicate every intra-cluster +* replacing in the body of the greatest predicate every intra-cluster call `Q(args)` to a greatest predicate by a call `Q#[_k - 1](args)` to the corresponding prefix predicate, and then -* prepending the body with `if _k = 0 then true else`. +* prepending the body with `if _k == 0 then true else`. -For example, for co-predicate `Pos`, the definition of the prefix +For example, for greatest predicate `Pos`, the definition of the prefix predicate `Pos#` is as suggested above. Syntactically, the prefix-length argument passed to a prefix predicate to indicate how many times to unroll the definition is written in square brackets, as in `Pos#[k](s)`. @@ -4049,7 +4050,7 @@ It has the usual equality syntax `s == t`, and the corresponding prefix equality is written `s ==#[k] t`. And similarly for `s != t` and `s !=#[k] t`. -### 19.3.5. Co-inductive Proofs +### 19.3.5. Coinductive Proofs From what we have said so far, a program can make use of properties of co-datatypes. For example, a method that declares `Pos(s)` as a precondition can rely on the stream `s` containing only positive integers. @@ -4057,22 +4058,22 @@ In this section, we consider how such properties are established in the first place. #### 19.3.5.1. Properties About Prefix Predicates -Among other possible strategies for establishing co-inductive properties -we take the time-honored approach of reducing co-induction to +Among other possible strategies for establishing coinductive properties +we take the time-honored approach of reducing coinduction to induction. More precisely, Dafny passes to the SMT solver an -assumption `D(P)` for every co-predicate `P`, where: +assumption `D(P)` for every greatest predicate `P`, where: ```dafny -D(P) = ? x • P(x) <==> ? k • P#[k](x) +D(P) = forall x • P(x) <==> forall k • P#[k](x) ``` -In other words, a co-predicate is true iff its corresponding prefix +In other words, a greatest predicate is true iff its corresponding prefix predicate is true for all finite unrollings. In Sec. 4 of the paper [Co-induction Simply] a soundness theorem of such -assumptions is given, provided the co-predicates meet the co-friendly +assumptions is given, provided the greatest predicates meet the continous restrictions. An example proof of `Pos(Up(n))` for every `n > 0` is -here shown: +shown here: ```dafny lemma UpPosLemma(n: int) @@ -4096,8 +4097,8 @@ lemma UpPosLemmaK(k: nat, n: int) The lemma `UpPosLemma` proves `Pos(Up(n))` for every `n > 0`. We first show `Pos#[k](Up(n ))`, for `n > 0` and an arbitrary `k`, and then use -the forall statement to show `? k • Pos#[k](Up(n))`. Finally, the axiom -`D(Pos)` is used (automatically) to establish the co-predicate. +the forall statement to show `forall k • Pos#[k](Up(n))`. Finally, the axiom +`D(Pos)` is used (automatically) to establish the greatest predicate. #### 19.3.5.2. Greatest lemmas {#sec-colemmas} @@ -4107,7 +4108,7 @@ predicate holds for all prefix lengths `k`. In this section, we introduce _greatest lemma_ declarations, which bring about two benefits. The first benefit is that greatest lemmas are syntactic sugar and reduce the tedium of having to write explicit quantifications over `k`. The second benefit is that, in -simple cases, the bodies of co-lemmas can be understood as co-inductive +simple cases, the bodies of greatest lemmas can be understood as coinductive proofs directly. As an example consider the following greatest lemma. ```dafny @@ -4118,7 +4119,7 @@ greatest lemma UpPosLemma(n: int) UpPosLemma(n+1); } ``` -This co-lemma can be understood as follows: `UpPosLemma` invokes itself +This greatest lemma can be understood as follows: `UpPosLemma` invokes itself co-recursively to obtain the proof for `Pos(Up(n).tail)` (since `Up(n).tail` equals `Up(n+1)`). The proof glue needed to then conclude `Pos(Up(n))` is provided automatically, thanks to the power of the SMT-based verifier. @@ -4132,44 +4133,44 @@ _prefix lemma_. In the call graph, the cluster containing a greatest lemma must contain only greatest lemmas and prefix lemmas, no other methods or function. By decree, a greatest lemma and its corresponding prefix lemma are always placed in the same cluster. Both greatest lemmas and prefix lemmas are always -ghosts. +ghost code. -The prefix lemma is constructed from the co-lemma by +The prefix lemma is constructed from the greatest lemma by * adding a parameter `_k` of type `nat` to denote the prefix length, -* replacing in the co-lemma’s postcondition the positive co-friendly - occurrences of co-predicates by corresponding prefix predicates, +* replacing in the greatest lemma’s postcondition the positive continuous + occurrences of greatest predicates by corresponding prefix predicates, passing in `_k` as the prefix-length argument, -* prepending `_k` to the (typically implicit) **decreases** clause of the co-lemma, +* prepending `_k` to the (typically implicit) **decreases** clause of the greatest lemma, -* replacing in the body of the co-lemma every intra-cluster call +* replacing in the body of the greatest lemma every intra-cluster call `M(args)` to a greatest lemma by a call `M#[_k - 1](args)` to the corresponding prefix lemma, and then * making the body’s execution conditional on `_k != 0`. -Note that this rewriting removes all co-recursive calls of co-lemmas, +Note that this rewriting removes all co-recursive calls of greatest lemmas, replacing them with recursive calls to prefix lemmas. These recursive -call are, as usual, checked to be terminating. We allow the pre-declared +calls are, as usual, checked to be terminating. We allow the pre-declared identifier `_k` to appear in the original body of the -co-lemma.[^fn-co-predicate-co-lemma-diffs] +greatest lemma.[^fn-co-predicate-co-lemma-diffs] [^fn-co-predicate-co-lemma-diffs]: Note, two places where co-predicates and co-lemmas are not analogous are (a) co-predicates must not make recursive calls to their prefix predicates and (b) co-predicates cannot mention `_k`. -We can now think of the body of the co-lemma as being replaced by a +We can now think of the body of the greatest lemma as being replaced by a **forall** call, for every _k_ , to the prefix lemma. By construction, this new body will establish the greatest lemma’s declared postcondition (on account of the `D` axiom, and remembering that only the positive -co-friendly occurrences of co-predicates in the co-lemma’s postcondition +continuous occurrences of greatest predicates in the greatest lemma’s postcondition are rewritten), so there is no reason for the program verifier to check it. -The actual desugaring of our co-lemma `UpPosLemma` is in fact the +The actual desugaring of our greatest lemma `UpPosLemma` is in fact the previous code for the `UpPosLemma` lemma except that `UpPosLemmaK` is named `UpPosLemma#` and modulo a minor syntactic difference in how the `k` argument is passed. @@ -4178,14 +4179,14 @@ In the recursive call of the prefix lemma, there is a proof obligation that the prefixlength argument `_k - 1` is a natural number. Conveniently, this follows from the fact that the body has been wrapped in an `if _k != 0` statement. This also means that the postcondition must -hold trivially when `_k = 0`, or else a postcondition violation will be +hold trivially when `_k == 0`, or else a postcondition violation will be reported. This is an appropriate design for our desugaring, because -co-lemmas are expected to be used to establish co-predicates, whose +greatest lemmas are expected to be used to establish greatest predicates, whose corresponding prefix predicates hold trivially when `_k = 0`. (To prove -other predicates, use an ordinary lemma, not a co-lemma.) +other predicates, use an ordinary lemma, not a greatest lemma.) It is interesting to compare the intuitive understanding of the -co-inductive proof in using a co-lemma with the inductive proof in using -the lemma. Whereas the inductive proof is performing proofs for deeper -and deeper equalities, the co-lemma can be understood as producing the +coinductive proof in using a greatest lemma with the inductive proof in using +a lemma. Whereas the inductive proof is performing proofs for deeper +and deeper equalities, the greatest lemma can be understood as producing the infinite proof on demand. diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 240e2987985..2bcda42ce05 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -954,7 +954,7 @@ implementation. `arr.Length`, or sequence length, etc. in executable code. You can however, use `arr.Length as uint64` if you can prove your array is an appropriate size. The compiler will report inappropriate integer use. -- We do not support more advanced Dafny features like traits or co-inductive +- We do not support more advanced Dafny features like traits or coinductive types. - Very limited support for higher order functions even for array init. Use extern definitions like newArrayFill (see @@ -1135,6 +1135,7 @@ code (which can be helpful for debugging). ``` ### 25.9.5. Controlling language features {#sec-controlling-language} +{#sec-function-syntax} These options allow some Dafny language features to be enabled or disabled. Some of these options exist for backward compatibility with diff --git a/docs/Snapshots.md b/docs/Snapshots.md index e1503fd874d..c3c8435f6a1 100644 --- a/docs/Snapshots.md +++ b/docs/Snapshots.md @@ -7,3 +7,6 @@ layout: default - [Current development version](https://dafny.org/dafny) - [Latest release snapshot](https://dafny.org/latest) +- [v3.9.0](https://davidcok.github.io/dafny-lang.github.io/v3.9.0) +- [v3.9.0](https://davidcok.github.io/dafny-lang.github.io/v3.9.0) +- [v3.9.0](https://davidcok.github.io/dafny-lang.github.io/v3.9.0)