Merge branch 'main' into semantics-of-reg-exp

Makefile

@@ -17,7 +17,8 @@ check:
 	assets/src/brittleness/verify.sh
 	assets/src/teaching-material/verify.sh
 	assets/src/standard-libraries/test.sh
-	assets/src/semantics-of-regular-expressions/verify.sh
+  assets/src/semantics-of-regular-expressions/verify.sh
+	(cd assets/src/clear-specification-and-implementation && ./verify.sh)
 
 generate:
 	node builders/verification-compelling-verify.js --regenerate _includes/verification-compelling-intro.html

assets/src/clear-specification-and-implementation/extract.sh

@@ -0,0 +1,17 @@
+#!/bin/sh
+print=0
+seen_stack=0
+IFS=
+while read line ; do
+  if [[ "$line" =~ "StackSpecification" ]] ; then
+    seen_stack=1
+  fi
+
+  if [[ "$line" =~ "{% highlight dafny %}" ]] ; then
+    print=1
+  elif [[ "$line" =~ "{% endhighlight %}" ]] ; then
+    print=0
+  elif [[ "$print" -eq 1 && "$seen_stack" -eq 1 ]] ; then
+    echo "$line"
+  fi
+done

assets/src/clear-specification-and-implementation/verify.sh

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+set -e
+
+if command -v dafny > /dev/null 2>&1
+then
+  echo
+  echo "*** Verification of the clear specification blog post"
+else
+    echo "Verification requires dafny to be installed"
+    exit 1
+fi
+
+./extract.sh < ../../../_posts/2023-08-15-clear-specification-and-implementation.markdown > clear-spec.dfy
+
+dafny verify clear-spec.dfy