fix: deprecated style: a semi-colon is not needed here (#143)

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

src/Collections/Sequences/Seq.dfy

@@ -48,15 +48,15 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Returns the last element of a non-empty sequence. */
   function Last<T>(xs: seq<T>): T
-    requires |xs| > 0;
+    requires |xs| > 0
   {
     xs[|xs|-1]
   }
 
   /* Returns the subsequence of a non-empty sequence obtained by
      dropping the last element. */
   function DropLast<T>(xs: seq<T>): seq<T>
-    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<T>(xs: seq<T>)
-    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<T>(xs: seq<T>, ys: seq<T>, zs: seq<T>)
-    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<T>(xs: seq<T>, 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<T>(xs: seq<T>, xs':seq<T>, 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<T>(xs: seq<T>, 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<T>(xs: seq<T>, ys: seq<T>)
-    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<T,R>(f: (T ~> R), xs: seq<T>): (result: seq<R>)
     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

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;

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

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<R>(escaped: StringBodyLexerState, byte: opt_byte)
       : LexerResult<StringBodyLexerState, R>
@@ -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<StringLexerState, string>

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)

src/JSON/ZeroCopy/Deserializer.dfy

@@ -28,7 +28,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
     type SubParser<!T> = Parsers.SubParser<T, JSONError>
 
     // 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<jchar>)
       ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, SpecView)
@@ -128,8 +128,8 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
     type TBracketed = Bracketed<jopen, TElement, jcomma, jclose>
     type TSuffixedElement = Suffixed<TElement, jcomma>
 
-    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)

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;

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)

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);
     }

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 {