Allow underscores in numeric literals (and in field/destructor names that are written as numeric strings). The

underscores have no semantic meaning, but can help a human parse the numbers.

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy
index a06f6c4a..1c1d7299 100644
--- a/Test/dafny4/BinarySearch.dfy
+++ b/Test/dafny4/BinarySearch.dfy
@@ -28,10 +28,10 @@ method BinarySearch(a: array<int>, key: int) returns (r: int)
 

 // Binary search using bounded integers

 

-newtype int32 = x | -0x80000000 <= x < 0x80000000

+newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000

 

 method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x80000000;

+  requires a != null && a.Length < 0x8000_0000;

   requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

   ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

   ensures r < 0 ==> key !in a[..];

@@ -54,7 +54,7 @@ method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)
 }

 

 method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x80000000;

+  requires a != null && a.Length < 0x8000_0000;

   requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

   ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

   ensures r < 0 ==> key !in a[..];