From 8b0c39969534dfdfb3b9fb4db777bf0cd97066a1 Mon Sep 17 00:00:00 2001 From: seebees Date: Tue, 26 Sep 2023 13:15:50 -0700 Subject: [PATCH] fix: deprecated style: a semi-colon is not needed here (#143) --- src/BoundedInts.dfy | 2 +- src/Collections/Sequences/Seq.dfy | 42 +++++++++---------- src/Collections/Sets/Sets.dfy | 2 +- src/JSON/Utils/Cursors.dfy | 2 +- src/JSON/Utils/Lexers.dfy | 4 +- src/JSON/Utils/Views.dfy | 2 +- src/JSON/ZeroCopy/Deserializer.dfy | 6 +-- src/JSON/ZeroCopy/Serializer.dfy | 4 +- .../Internals/ModInternals.dfy | 2 +- src/NonlinearArithmetic/Mul.dfy | 6 +-- src/NonlinearArithmetic/Power.dfy | 2 +- 11 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy index 33768d5d..d479f3bf 100644 --- a/src/BoundedInts.dfy +++ b/src/BoundedInts.dfy @@ -17,7 +17,7 @@ module {:options "-functionSyntax:4"} BoundedInts { const TWO_TO_THE_128: int := 0x1_00000000_00000000_00000000_00000000 const TWO_TO_THE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 const TWO_TO_THE_512: int := - 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; + 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 newtype uint8 = x: int | 0 <= x < TWO_TO_THE_8 newtype uint16 = x: int | 0 <= x < TWO_TO_THE_16 diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index a71a487c..d98dcd0b 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -48,7 +48,7 @@ module {:options "-functionSyntax:4"} Seq { /* Returns the last element of a non-empty sequence. */ function Last(xs: seq): T - requires |xs| > 0; + requires |xs| > 0 { xs[|xs|-1] } @@ -56,7 +56,7 @@ module {:options "-functionSyntax:4"} Seq { /* Returns the subsequence of a non-empty sequence obtained by dropping the last element. */ function DropLast(xs: seq): seq - requires |xs| > 0; + requires |xs| > 0 { xs[..|xs|-1] } @@ -65,8 +65,8 @@ module {:options "-functionSyntax:4"} Seq { from dropping the last element, the second consisting only of the last element, is the original sequence. */ lemma LemmaLast(xs: seq) - requires |xs| > 0; - ensures DropLast(xs) + [Last(xs)] == xs; + requires |xs| > 0 + ensures DropLast(xs) + [Last(xs)] == xs { } @@ -80,7 +80,7 @@ module {:options "-functionSyntax:4"} Seq { /* The concatenation of sequences is associative. */ lemma LemmaConcatIsAssociative(xs: seq, ys: seq, zs: seq) - ensures xs + (ys + zs) == (xs + ys) + zs; + ensures xs + (ys + zs) == (xs + ys) + zs { } @@ -128,33 +128,33 @@ module {:options "-functionSyntax:4"} Seq { with that same sequence sliced from the pos-th element, is equal to the original unsliced sequence. */ lemma LemmaSplitAt(xs: seq, pos: nat) - requires pos < |xs|; - ensures xs[..pos] + xs[pos..] == xs; + requires pos < |xs| + ensures xs[..pos] + xs[pos..] == xs { } /* Any element in a slice is included in the original sequence. */ lemma LemmaElementFromSlice(xs: seq, xs':seq, a: int, b: int, pos: nat) - requires 0 <= a <= b <= |xs|; - requires xs' == xs[a..b]; - requires a <= pos < b; - ensures pos - a < |xs'|; - ensures xs'[pos-a] == xs[pos]; + requires 0 <= a <= b <= |xs| + requires xs' == xs[a..b] + requires a <= pos < b + ensures pos - a < |xs'| + ensures xs'[pos-a] == xs[pos] { } /* A slice (from s2..e2) of a slice (from s1..e1) of a sequence is equal to just a slice (s1+s2..s1+e2) of the original sequence. */ lemma LemmaSliceOfSlice(xs: seq, s1: int, e1: int, s2: int, e2: int) - requires 0 <= s1 <= e1 <= |xs|; - requires 0 <= s2 <= e2 <= e1 - s1; - ensures xs[s1..e1][s2..e2] == xs[s1+s2..s1+e2]; + requires 0 <= s1 <= e1 <= |xs| + requires 0 <= s2 <= e2 <= e1 - s1 + ensures xs[s1..e1][s2..e2] == xs[s1+s2..s1+e2] { var r1 := xs[s1..e1]; var r2 := r1[s2..e2]; var r3 := xs[s1+s2..s1+e2]; assert |r2| == |r3|; - forall i {:trigger r2[i], r3[i]}| 0 <= i < |r2| ensures r2[i] == r3[i]; + forall i {:trigger r2[i], r3[i]}| 0 <= i < |r2| ensures r2[i] == r3[i] { } } @@ -208,10 +208,10 @@ module {:options "-functionSyntax:4"} Seq { elements in common between them, then the concatenated sequence xs + ys will not contain duplicates either. */ lemma {:timeLimitMultiplier 3} LemmaNoDuplicatesInConcat(xs: seq, ys: seq) - requires HasNoDuplicates(xs); - requires HasNoDuplicates(ys); - requires multiset(xs) !! multiset(ys); - ensures HasNoDuplicates(xs+ys); + requires HasNoDuplicates(xs) + requires HasNoDuplicates(ys) + requires multiset(xs) !! multiset(ys) + ensures HasNoDuplicates(xs+ys) { reveal HasNoDuplicates(); var zs := xs + ys; @@ -620,7 +620,7 @@ module {:options "-functionSyntax:4"} Seq { function {:opaque} Map(f: (T ~> R), xs: seq): (result: seq) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) ensures |result| == |xs| - ensures forall i {:trigger result[i]} :: 0 <= i < |xs| ==> result[i] == f(xs[i]); + ensures forall i {:trigger result[i]} :: 0 <= i < |xs| ==> result[i] == f(xs[i]) reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o { // This uses a sequence comprehension because it will usually be diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index 70bf5078..6b6d7191 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -231,7 +231,7 @@ module {:options "-functionSyntax:4"} Sets { { var range := SetRange(a, b); forall e {:trigger e in range}{:trigger e in x} | e in x - ensures e in range; + ensures e in range { } assert x <= range; diff --git a/src/JSON/Utils/Cursors.dfy b/src/JSON/Utils/Cursors.dfy index 2a6236e9..5be9838e 100644 --- a/src/JSON/Utils/Cursors.dfy +++ b/src/JSON/Utils/Cursors.dfy @@ -55,7 +55,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Cursors { datatype Cursor_ = Cursor(s: bytes, beg: uint32, point: uint32, end: uint32) { ghost const Valid?: bool := - 0 <= beg as int <= point as int <= end as int <= |s| < TWO_TO_THE_32; + 0 <= beg as int <= point as int <= end as int <= |s| < TWO_TO_THE_32 const BOF? := point == beg diff --git a/src/JSON/Utils/Lexers.dfy b/src/JSON/Utils/Lexers.dfy index a600b3a5..aaa9b3e7 100644 --- a/src/JSON/Utils/Lexers.dfy +++ b/src/JSON/Utils/Lexers.dfy @@ -22,7 +22,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Lexers { import opened BoundedInts type StringBodyLexerState = /* escaped: */ bool - const StringBodyLexerStart: StringBodyLexerState := false; + const StringBodyLexerStart: StringBodyLexerState := false function StringBody(escaped: StringBodyLexerState, byte: opt_byte) : LexerResult @@ -33,7 +33,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Lexers { } datatype StringLexerState = Start | Body(escaped: bool) | End - const StringLexerStart: StringLexerState := Start; + const StringLexerStart: StringLexerState := Start function String(st: StringLexerState, byte: opt_byte) : LexerResult diff --git a/src/JSON/Utils/Views.dfy b/src/JSON/Utils/Views.dfy index d655b359..4fcafef5 100644 --- a/src/JSON/Utils/Views.dfy +++ b/src/JSON/Utils/Views.dfy @@ -8,7 +8,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Views.Core { type View = v: View_ | v.Valid? witness View([], 0, 0) datatype View_ = View(s: bytes, beg: uint32, end: uint32) { ghost const Valid?: bool := - 0 <= beg as int <= end as int <= |s| < TWO_TO_THE_32; + 0 <= beg as int <= end as int <= |s| < TWO_TO_THE_32 static const Empty: View := View([], 0, 0) diff --git a/src/JSON/ZeroCopy/Deserializer.dfy b/src/JSON/ZeroCopy/Deserializer.dfy index 0b7212f9..898af31f 100644 --- a/src/JSON/ZeroCopy/Deserializer.dfy +++ b/src/JSON/ZeroCopy/Deserializer.dfy @@ -28,7 +28,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer { type SubParser = Parsers.SubParser // BUG(https://github.com/dafny-lang/dafny/issues/2179) - const SpecView := (v: Vs.View) => Spec.View(v); + const SpecView := (v: Vs.View) => Spec.View(v) function {:opaque} Get(cs: FreshCursor, err: JSONError): (pr: ParseResult) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, SpecView) @@ -128,8 +128,8 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer { type TBracketed = Bracketed type TSuffixedElement = Suffixed - const SpecViewClose: jclose -> bytes := SpecView; - const SpecViewOpen: jopen -> bytes := SpecView; + const SpecViewClose: jclose -> bytes := SpecView + const SpecViewOpen: jopen -> bytes := SpecView ghost function SuffixedElementSpec(e: TSuffixedElement): bytes { ElementSpec(e.t) + Spec.CommaSuffix(e.suffix) diff --git a/src/JSON/ZeroCopy/Serializer.dfy b/src/JSON/ZeroCopy/Serializer.dfy index 8746fdb6..796fa5da 100644 --- a/src/JSON/ZeroCopy/Serializer.dfy +++ b/src/JSON/ZeroCopy/Serializer.dfy @@ -269,7 +269,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Serializer { method MembersImpl(obj: jobject, writer: Writer) returns (wr: Writer) decreases obj, 1 - ensures wr == MembersSpec(obj, obj.data, writer); + ensures wr == MembersSpec(obj, obj.data, writer) { wr := writer; var members := obj.data; @@ -286,7 +286,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Serializer { method {:vcs_split_on_every_assert} ItemsImpl(arr: jarray, writer: Writer) returns (wr: Writer) decreases arr, 1 - ensures wr == ItemsSpec(arr, arr.data, writer); + ensures wr == ItemsSpec(arr, arr.data, writer) { wr := writer; var items := arr.data; diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy index d192970e..388b06f1 100644 --- a/src/NonlinearArithmetic/Internals/ModInternals.dfy +++ b/src/NonlinearArithmetic/Internals/ModInternals.dfy @@ -199,7 +199,7 @@ module {:options "-functionSyntax:4"} ModInternals { /* automates the modulus operator process */ ghost predicate ModAuto(n: int) - requires n > 0; + requires n > 0 { && (n % n == (-n) % n == 0) && (forall x: int {:trigger (x % n) % n} :: (x % n) % n == x % n) diff --git a/src/NonlinearArithmetic/Mul.dfy b/src/NonlinearArithmetic/Mul.dfy index 805a38c0..129cf12a 100644 --- a/src/NonlinearArithmetic/Mul.dfy +++ b/src/NonlinearArithmetic/Mul.dfy @@ -79,7 +79,7 @@ module {:options "-functionSyntax:4"} Mul { ensures forall x: int, y: int {:trigger x * y} :: x * y != 0 <==> x != 0 && y != 0 { forall (x: int, y: int) - ensures x * y != 0 <==> x != 0 && y != 0; + ensures x * y != 0 <==> x != 0 && y != 0 { LemmaMulNonzero(x, y); } @@ -332,7 +332,7 @@ module {:options "-functionSyntax:4"} Mul { ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x * z < y * z && z >= 0 ==> x < y { forall (x: int, y: int, z: int | x * z < y * z && z >= 0) - ensures x < y; + ensures x < y { LemmaMulStrictInequalityConverse(x, y, z); } @@ -385,7 +385,7 @@ module {:options "-functionSyntax:4"} Mul { ensures forall x: int, y: int, z: int {:trigger x * (y - z)} :: x * (y - z) == x * y - x * z { forall (x: int, y: int, z: int) - ensures x * (y - z) == x * y - x * z; + ensures x * (y - z) == x * y - x * z { LemmaMulIsDistributiveSub(x, y, z); } diff --git a/src/NonlinearArithmetic/Power.dfy b/src/NonlinearArithmetic/Power.dfy index 4e55851d..a3b24650 100644 --- a/src/NonlinearArithmetic/Power.dfy +++ b/src/NonlinearArithmetic/Power.dfy @@ -574,7 +574,7 @@ module {:options "-functionSyntax:4"} Power { /* b^e % b = 0 */ lemma LemmaPowMod(b: nat, e: nat) requires b > 0 && e > 0 - ensures Pow(b, e) % b == 0; + ensures Pow(b, e) % b == 0 { reveal Pow(); calc {