Add Dafny runtime tests to CI

Author: shaobo-he

.github/workflows/ci.yaml

@@ -23,19 +23,24 @@ jobs:
           wget -q https://github.com/dafny-lang/dafny/releases/download/v4.11.0/dafny-4.11.0-x64-ubuntu-22.04.zip
           unzip -qq dafny-4.11.0-x64-ubuntu-22.04.zip
           echo "dafny=$PWD/dafny/dafny" >> $GITHUB_ENV
-      - name: test
+      - name: verify and test
         env:
           DAFNY: "${{ env.dafny }}"
           TEST_DIR: "${{ matrix.test_dir }}"
         run: |
-          for b in $(ls $TEST_DIR/*.dfy)
+          set -euo pipefail
+          shopt -s nullglob
+          for b in "$TEST_DIR"/*.dfy
           do
-            echo $b
+            echo "$b"
             if [[ "$b" == *"[wip]"* ]]
             then
-              echo "Ignore working in progress proof: "$b
+              echo "Ignore working in progress proof: $b"
+            elif grep -q '{:test}' "$b"
+            then
+              "$DAFNY" test --verification-time-limit 30 "$b"
             else
-              $DAFNY verify "$b"
+              "$DAFNY" verify --verification-time-limit 30 "$b"
             fi
             echo "================================================"
           done

.gitignore

@@ -3,4 +3,12 @@ bin/
 leetcode/*.txt
 lib/**/Work*
 *.dll
-*.json
+*.json
+
+# Generated by `dafny test` when using the default C# target.
+*.cs
+*.csproj
+*.exe
+*.pdb
+obj/
+**/obj/

leetcode/0001-two-sum.dfy

@@ -40,4 +40,17 @@ method TwoSum(nums: array<int>, target: int) returns (r: (int, int))
     i := i + 1;
   }
   return (-1, -1);
-}
+}
+
+method {:test} TestTwoSum()
+{
+  var nums := new int[4];
+  nums[0], nums[1], nums[2], nums[3] := 2, 7, 11, 15;
+  var r := TwoSum(nums, 9);
+  expect r == (0, 1), "[2,7,11,15], target 9 should return (0,1)";
+
+  var none := new int[3];
+  none[0], none[1], none[2] := 1, 2, 4;
+  var missing := TwoSum(none, 8);
+  expect missing == (-1, -1), "no-solution case should return (-1,-1)";
+}

leetcode/0004-median-two-sorted-arrays.dfy

@@ -464,3 +464,15 @@ lemma ExampleEven()
   assert Merge([1, 2], [3, 4]) == [1, 2, 3, 4];
   MergeLen([1, 2], [3, 4]);
 }
+
+method {:test} TestFindMedianSortedArraysX2()
+{
+  var odd := FindMedianSortedArraysX2([1, 3], [2]);
+  expect odd == 4, "median of [1,3] and [2] should be 2.0";
+
+  var even := FindMedianSortedArraysX2([1, 2], [3, 4]);
+  expect even == 5, "median of [1,2] and [3,4] should be 2.5";
+
+  var swapped := FindMedianSortedArraysX2([3, 4], [1, 2]);
+  expect swapped == 5, "median should be independent of argument order";
+}

leetcode/0146-lru-cache.dfy

@@ -396,3 +396,27 @@ class LRUCache {
     }
   }
 }
+
+method {:test} TestLRUCache()
+{
+  var cache := new LRUCache(2);
+  cache.Put(1, 1);
+  cache.Put(2, 2);
+
+  var one := cache.Get(1);
+  expect one == 1, "Get(1) should return 1";
+
+  cache.Put(3, 3);
+  var evictedTwo := cache.Get(2);
+  expect evictedTwo == -1, "Put(3,3) should evict key 2";
+
+  cache.Put(4, 4);
+  var evictedOne := cache.Get(1);
+  expect evictedOne == -1, "Put(4,4) should evict key 1";
+
+  var three := cache.Get(3);
+  expect three == 3, "Get(3) should return 3";
+
+  var four := cache.Get(4);
+  expect four == 4, "Get(4) should return 4";
+}

leetcode/0155-min-stack.dfy

@@ -155,4 +155,24 @@ class MinStack {
 //   {
 //     return Last(mins);
 //   }
-// }
+// }
+
+method {:test} TestMinStack()
+{
+  var stack := new MinStack();
+  stack.Push(-2);
+  stack.Push(0);
+  stack.Push(-3);
+
+  var min1 := stack.GetMin();
+  expect min1 == -3, "minimum should be -3";
+
+  var popped := stack.Pop();
+  expect popped == -3, "pop should remove -3";
+
+  var top := stack.Top();
+  expect top == 0, "top should be 0";
+
+  var min2 := stack.GetMin();
+  expect min2 == -2, "minimum should be -2 after popping -3";
+}

leetcode/0312-burst-balloons.dfy

@@ -352,3 +352,18 @@ lemma BruteVsBestTwo()
 {
   BestEqualsBruteMaxPair(3, 1);
 }
+
+method {:test} TestBurstBalloons()
+{
+  var empty := BurstBalloons([]);
+  expect empty == 0, "empty input should score 0";
+
+  var single := BurstBalloons([5]);
+  expect single == 5, "single balloon [5] should score 5";
+
+  var pair := BurstBalloons([3, 1]);
+  expect pair == 6, "[3,1] should score 6";
+
+  var leet := BurstBalloons([3, 1, 5, 8]);
+  expect leet == 167, "[3,1,5,8] should score 167";
+}

leetcode/0407-trapping-rain-water-ii-correct.dfy

@@ -526,3 +526,12 @@ ExampleBowl()
           Vol(EscGrid(H, 5, 1), H) == 4
 {
 }
+
+method {:test} TestTrappingRainWaterByEscapeLevels()
+{
+  var bowl := TrappingRainWater([[5, 5, 5], [5, 1, 5], [5, 5, 5]]);
+  expect bowl == 4, "3x3 bowl should trap 4";
+
+  var flat := TrappingRainWater([[1, 1], [1, 1]]);
+  expect flat == 0, "boundary-only grid should trap 0";
+}

leetcode/0407-trapping-rain-water-ii.dfy

@@ -178,3 +178,12 @@ method HeapFloodTrappingRainWater(heightMap: seq<seq<int>>) returns (water: int)
                        water == Vol(L, heightMap);
   }
 }
+
+method {:test} TestHeapFloodBoundaryOnly()
+{
+  var oneRow := HeapFloodTrappingRainWater([[1, 4, 2]]);
+  expect oneRow == 0, "single-row grid should trap 0";
+
+  var twoRows := HeapFloodTrappingRainWater([[3, 1, 3], [3, 3, 3]]);
+  expect twoRows == 0, "two-row grid should trap 0";
+}