Merge pull request #117 from JstnMcBrd/dafny

Add Dafny implementation
mawerty · Jan 11, 2024 · 683aa57 · 683aa57
2 parents cfb5808 + dc537ab
commit 683aa57
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -42,6 +42,7 @@ C++
 C#
 CSS
 CUDA
+Dafny
 Dart
 Elixir
 Elm

diff --git a/implementations/main.dfy b/implementations/main.dfy
@@ -0,0 +1,11 @@
+predicate is_prime(number: int)
+{
+    false
+}
+
+// Because Dafny is a formal verification language, assertions to prove correctness
+// are necessary for the program to have any meaning.
+method {:test} test()
+{
+    assert forall n :: n in [4, 6, 8, 9, 10] ==> !is_prime(n);
+}
diff --git a/optimized_implementations/main.dfy b/optimized_implementations/main.dfy
@@ -0,0 +1,2 @@
+predicate is_prime(n:int){false}
+method{:test}test(){assert forall n::n in [4,6,8,9,10] ==> !is_prime(n);}
-Original file line number
+Diff line change
@@ Expand Up / @@ -42,6 +42,7 @@ C++ @@
     C#
     CSS
     CUDA
+    Dafny
     Dart
     Elixir
     Elm
@@ Expand Down @@
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		predicate is_prime(n:int){false}
		method{:test}test(){assert forall n::n in [4,6,8,9,10] ==> !is_prime(n);}