update verus intro slides, exercises

verus-lang · Nov 2, 2024 · 58747af · 58747af
1 parent b5d0876
commit 58747af
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 0 deletions.
diff --git a/2024-sosp-tutorial/exercises/verus-intro/exercise_smallest_elt.rs b/2024-sosp-tutorial/exercises/verus-intro/exercise_smallest_elt.rs
@@ -24,6 +24,9 @@ fn smallest_elt(elts: Vec<u64>) -> (result: u64)
 }
 
 fn main() {
+    let v = vec![3,1,2];
+    let e = smallest_elt(v);
+    assert(e == 1);
 }
 
 }
diff --git a/2024-sosp-tutorial/exercises/verus-intro/solutions/solution_smallest_elt.rs b/2024-sosp-tutorial/exercises/verus-intro/solutions/solution_smallest_elt.rs
@@ -25,6 +25,9 @@ fn smallest_elt(elts: Vec<u64>) -> (result: u64)
 }
 
 fn main() {
+    let v = vec![3,1,2];
+    let e = smallest_elt(v);
+    assert(e == 1);
 }
 
 }
diff --git a/2024-sosp-tutorial/slides/02-verus.key b/2024-sosp-tutorial/slides/02-verus.key
diff --git a/2024-sosp-tutorial/slides/02-verus.pptx b/2024-sosp-tutorial/slides/02-verus.pptx