use dafny syntax highlighting

_posts/2023-07-14-types-and-programming-languages.markdown

@@ -46,7 +46,7 @@ Writing a type-checker that guarantees that evaluation of a term won't get stuck
 
 First, let's define the term language used in the Blockly interface above. Note that the logic of the Blockly workspace above uses that exact code written on this page. Yeah, Dafny compiles to JavaScript too!
 
-{% highlight javascript %}
+{% highlight dafny %}
 datatype Term  =
   | True
   | False
@@ -63,7 +63,7 @@ datatype Term  =
 
 Let's also add the two types our expressions can have.
 
-{% highlight javascript %}
+{% highlight dafny %}
 datatype Type =
   | Bool
   | Int
@@ -74,7 +74,7 @@ datatype Type =
 We can now write a _type checker_ for the terms above. In our case, a type checker will take a term, and return a type if the term has that type. We will not dive into error reporting in this blog post.
 First, because a term may or may not have a type, we want an `Option<A>` type like this:
 
-{% highlight javascript %}
+{% highlight dafny %}
 datatype Option<A> = Some(value: A) | None
 {% endhighlight %}
 
@@ -83,7 +83,7 @@ For example, in a conditional term, the condition has to be a boolean,
 while we only require the "then" and "else" part to have the same, defined type.
 In general, computing types is a task linear in the size of the code, whereas evaluating the code could have any complexity. This is why type checking is an efficient way of preventing obvious mistakes.
 
-{% highlight javascript %}
+{% highlight dafny %}
 function GetType(term: Term): Option<Type> {
   match term {
     case True  => Some(Bool)
@@ -132,7 +132,7 @@ function GetType(term: Term): Option<Type> {
 
 A well-typed term is one for which a type exists.
 
-{% highlight javascript %}
+{% highlight dafny %}
 predicate WellTyped(term: Term) {
   GetType(term) != None
 }
@@ -146,7 +146,7 @@ At first, we can define the notion of evaluating a term. We can evaluate a term
 There are terms where no replacement is possible: value terms.
 Here is what we want them to look like: either booleans, zero, positive integers, or negative integers.
 
-{% highlight javascript %}
+{% highlight dafny %}
 predicate IsSuccs(term: Term) {
   term == Zero || (term.Succ? && IsSuccs(term.e))
 }
@@ -161,7 +161,7 @@ predicate IsFinalValue(term: Term) {
 
 Now, we can write our one-step evaluation method. As a requirement, we add that the term must be well-typed and nonfinal.
 
-{% highlight javascript %}
+{% highlight dafny %}
 function OneStepEvaluate(e: Term): (r: Term)
   requires WellTyped(e) && !IsFinalValue(e)
 {
@@ -238,7 +238,7 @@ That concludes the _progress_ part of soundness checking: whenever a term type-c
 Soundness has another aspect, preservation, as stated in the intro. It says that, when evaluating a well-typed term, the evaluator will not get stuck and the result will have the same type as the original term.
 Dafny can also prove it for our language, out of the box. Well done, that means our language and evaluator make sense together!
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma OneStepEvaluateWellTyped(e: Term)
   requires WellTyped(e) && !IsFinalValue(e)
   ensures GetType(OneStepEvaluate(e)) == GetType(e)
@@ -281,7 +281,7 @@ Note that these terms omit `Double` and `Add` above. This means we cannot state
 
 We can write the inductive definition above in Dafny too:
 
-{% highlight javascript %}
+{% highlight dafny %}
 ghost const AllTermsInductively: iset<Term>
 
 ghost predicate InductionCriteria(terms: iset<Term>) {
@@ -305,7 +305,7 @@ $$\begin{aligned}S_{i+1} = && && \{\texttt{true}, \texttt{false}, 0\} \\ && \big
 
 This we can enter in Dafny too:
 
-{% highlight javascript %}
+{% highlight dafny %}
 ghost function S(i: nat): iset<Term> {
   if i == 0 then
     iset{}
@@ -342,7 +342,7 @@ between any two sets.
 We use the annotation `{:vcs_split_on_every_assert}` which makes Dafny verify each assertion independently, which, in this example, helps the verifier. Yes, [helping the verifier](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-verification-debugging-slow) is something we must occasionally do in Dafny.
 To further control the situation, we use the annotation `{:induction false}` to ensure Dafny does not try to prove induction hypotheses by itself, which gives us control over the proof. Otherwise, Dafny can both automate the proof a lot (which is great!) and sometimes time out because automation is stuck (which is less great!). I left assertions in the code so that not only Dafny, but you too can understand the proof.
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma {:vcs_split_on_every_assert} {:induction false} SiAreCumulative(i: nat)
   ensures S(i) <= S(i+1)
 {
@@ -403,7 +403,7 @@ After proving that intermediate sets form an increasing sequence, we want to pro
 
 Note that I use the annotation `{:rlimit 4000}` which is only a way for Dafny to say that every [assertion batch](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-assertion-batches) should verify using less than 4 million resource units (unit provided by the underlying solver), which reduces the chances of proof variability during development.
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma {:rlimit 4000} {:vcs_split_on_every_assert}
   AllTermsConstructivelySatisfiesInductionCriteria()
   ensures InductionCriteria(AllTermsConstructively)
@@ -449,7 +449,7 @@ lemma {:rlimit 4000} {:vcs_split_on_every_assert}
 Now we want to prove that every `S(i)` is included in every set that satisfies the induction criteria. That way, their union, the constructive set, will also be included in any set that satisfies the induction criteria. The proof works by remarking that every element of `S(i)` is built from elements of `S(i-1)`, so if these elements are in the set satisfying the induction criteria, so is the element by induction.
 I intentionally detailed the proof so that you can understand it, but if you run it yourself, you might see that you can remove a lot of the proof and Dafny will still figure it out.
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma {:induction false}
   InductionCriteriaHasConcreteIAsSubset(
     i: nat, someset: iset<Term>
@@ -510,7 +510,7 @@ lemma {:induction false}
 
 We can deduce from the previous result that the constructive definition of all terms is also included in any set of term that satisfies the induction criteria. From this we can deduce automatically that the constructive definition of all terms is included in the smallest inductive set satisfying the induction criteria.
 
-{% highlight javascript %}
+{% highlight dafny %}
 // 3.2.6.b.1 AllTermsConstructively is a subset of any set satisfying the induction criteria (hence AllTermsConstructively <= AllTermsInductively)
 lemma AllTermsConstructivelyIncludedInSetsSatisfyingInductionCriteria(
   terms: iset<Term>
@@ -535,7 +535,7 @@ lemma AllTermsConstructivelyIncludedInAllTermsInductively()
 
 Because we have `<=` and `>=` between these two sets, we can now prove equality.
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma InductionAndConcreteAreTheSame()
   ensures AllTermsConstructively == AllTermsInductively
 {
@@ -552,7 +552,7 @@ As stated in the introduction, having multiple definitions of a single infinite
 
 - If a term is in the constructive set, then it cannot be constructed with `Add` for example, because it would need to be in a `S(i)` and none of the `S(i)` define `Add`. This can be illustrated in Dafny with the following lemma:
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma {:induction false} CannotBeAdd(t: Term)
   requires t in AllTermsConstructively
   ensures !t.Add?
@@ -566,7 +566,7 @@ which Dafny can verify pretty easily. However, if you put `AllTermsInductively`
 - If `x` is in the inductive set, then `Succ(x)` is in the inductive set as well.
 Dafny can figure it out by itself using the `AllTermsInductively` definition, but won't be able to do it with `AllTermsConstructively` without a rigorous proof.
 
-{% highlight javascript %}
+{% highlight dafny %}
 lemma {:induction false} SuccIsInInductiveSet(t: Term)
   requires t in AllTermsInductively
   ensures Succ(t) in AllTermsInductively
@@ -580,7 +580,7 @@ This could be useful for a rewriter or an optimizer to ensure the elements it wr
 Everything said, everything above can be a bit overweight for regular Dafny users.
 In practice, you're better off writing the inductive predicate explicitly as a function rather than an infinite set with a predicate, so that you get both inductive and constructive axioms that enable you to prove something similar to the two results above.
 
-{% highlight javascript %}
+{% highlight dafny %}
 predicate IsAdmissible(t: Term) {
   match t {
     case True => true

_posts/2023-11-08-cracking-the-coding-interview-in-dafny-permutations.markdown

@@ -21,15 +21,15 @@ The coding interview problem is described to us in natural language. As we would
 
 Intuitively, a *permutation* of a sequence is a second sequence that contains the same elements as the first one, but potentially in a different order. In other words, after *one forgets about the order* of the elements, both structures are identical.  For example, the sequence `[1,0,0]` is a permutation of the sequence `[0,0,1]`. In Dafny, a sequence without an order can be modeled by the type [`multiset`](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-multisets). Multisets are generalisations of sets in the way that they can contain elements *multi*ple times, instead of just once. The multiset that models both of the above sequences is `multiset{0,0,1}` . Note that this multiset is different from the set  `set{0,0,1} == set{0,1}`. You may think of multisets that contain elements of type `T` as functions `f: T -> nat` , where `f(t)` specifies how many occurrences of the element `t` the multiset contains. In Dafny, the conversion of a sequence `s` into a multiset is denoted by `multiset(s)` . We define a sequence `p` to be a permutation of a sequence `s` (both with elements of a generic type `T`) if they satisfy the following predicate:
 
-```
+``` dafny
 predicate IsPermutationOf<T(==)>(p: seq<T>, s: seq<T>) {
   multiset(p) == multiset(s)
 }
 ```
 
 Note that a predicate is a function that returns a `bool`ean — that is, either `true` or `false`. To compare two multisets for equality, we need to be able to compare their elements for equality. For this reason, we require the type `T` to have the characteristic [`(==)`](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-equality-supporting). Given above, the naive definition of the set that contains all permutations of a sequence `s` is immediate:
 
-```
+``` dafny
 ghost function AllPermutationsOf<T(!new)>(s: seq<T>): iset<seq<T>> {
   iset p | IsPermutationOf(p, s)
 }
@@ -39,13 +39,13 @@ Note that `AllPermutationsOf` returns a potentially *infinite* set of sequences.
 
 We are now able to formally state the problem task: Define the body of a function with the signature
 
-```
+``` dafny
 function CalculateAllPermutationsOf<T(==)>(s: seq<T>): set<seq<T>>
 ```
 
 and show that it is *correct*, in the sense that there exists a proof for the lemma
 
-```
+``` dafny
 lemma Correctness<T(!new)>(s: seq<T>)
   ensures (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s)
 ```
@@ -54,7 +54,7 @@ lemma Correctness<T(!new)>(s: seq<T>)
 
 There are many potential solutions to the problem. Here, we propose a purely functional approach that defines the set of all unique permutations of a sequence recursively. In the base case, when the sequence `s` has length zero, we simply return the singleton set that contains `s`. In the case that `s` is of length greater than zero, we first recursively calculate the set of all the permutations of the subsequence of `s` that starts at the second element, before inserting, via a separate function `InsertAt`, the first element of `s` into all the permutations in that set, at every possible position.
 
-```
+``` dafny
 function CalculateAllPermutationsOf<T(==)>(s: seq<T>): set<seq<T>> {
   if |s| == 0 then
     {s}
@@ -72,7 +72,7 @@ function InsertAt<T>(s: seq<T>, x: T, i: nat): seq<T>
 
 For example, to compute the set of all permutations of the sequence `s := [0,0,1]` , we first compute the set of all unique permutations of the subsequence `s[1..] == [0,1]` , which leads to `{[0,1], [1,0]}`. Then we insert the first element `s[0] == 0` into all the sequences of that set, at every possible position. In this case, the resulting set is `{[0,0,1], [0,1,0], [1,0,0]}`, as indicated below:
 
-```
+``` dafny
 {
  [0] + [0,1], [0] + [0] + [1], [0,1] + [0], // inserting 0 into [0,1]
  [0] + [1,0], [1] + [0] + [0], [1,0] + [0]  // inserting 0 into [1,0]
@@ -85,7 +85,7 @@ During a coding interview, the focus would now typically shift to an analysis of
 
 To establish correctness, we need to prove, for all sequences `s`, the equality of the two (infinite) sets `A(s) := iset p | p in CalculateAllPermutationsOf(s)` and `B(s) := AllPermutationsOf(s)`. That is, we have to establish the validity of two implications, for all sequences `p`: i) if `p` is in `A(s)` , then it also is in `B(s)`; and ii) if `p` is in `B(s)` , then it also is in `A(s)`. We prove the two cases in separate lemmas `CorrectnessImplicationOne(s, p)` and `CorrectnessImplicationTwo(s, p)`, respectively:
 
-```
+``` dafny
 lemma Correctness<T(!new)>(s: seq<T>)
   ensures (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s)
 {
@@ -118,7 +118,7 @@ The first implication is arguably the more intuitive or simpler one to prove. It
 
 As is typical for Dafny, the proof of the lemma follows the structure of the function that it reasons about. In this case, we mimic the function `CalculateAllPermutationsOf` by mirroring its recursive nature as a proof via induction. In particular, this means that we copy its case-split. In the case that `s` is of length zero (the induction base), Dafny is able to prove the claim automatically: 
 
-```
+``` dafny
 lemma CorrectnessImplicationOne<T(!new)>(s: seq<T>, p: seq<T>)
   ensures p in CalculateAllPermutationsOf(s) ==> p in AllPermutationsOf(s)
 {
@@ -150,7 +150,7 @@ lemma CorrectnessImplicationOne<T(!new)>(s: seq<T>, p: seq<T>)
 
 In the case that `s` is of length greater than zero (the induction step), we need to help Dafny a bit. Assuming that `p` is an element in `CalculateAllPermutationsOf(s)`, we aim to show that  `multiset(p)` and `multiset(s)` are equal. What information about `p` do we have to derive such an equality? A close inspection of the recursive call in `CalculateAllPermutationsOf` indicates the existence of a second sequence `p’`  that lives in `CalculateAllPermutationsOf(s[1..])` and an index `i` of `p’` such that  `p == InsertAt(p', s[0], i)` . To transform `multiset(p) == multiset(InsertAt(p', s[0], i))` into something that’s closer to `multiset(s)`, we establish the following additional lemma:
 
-```
+``` dafny
 lemma MultisetAfterInsertAt<T>(s: seq<T>, x: T, i: nat)
   requires i <= |s|
   ensures multiset(InsertAt(s, x, i)) == multiset([x]) + multiset(s)
@@ -178,7 +178,7 @@ The second implication states that any permutation `p` of `s` is an element of `
 
 As with the first implication, the structure of the proof for `CorrectnessImplicationTwo` mimics the definition of `CalculateAllPermutationsOf`. In the case that `s` is of length zero (the induction base), Dafny is again able to prove the claim automatically. In the case that `s` is of length greater than zero (the induction step), we aim to establish that `p` is an element in `CalculateAllPermutationsOf(s)`, if it is a permutation of `s`:
 
-```
+``` dafny
 lemma CorrectnessImplicationTwo<T(!new)>(s: seq<T>, p: seq<T>)
   ensures p in CalculateAllPermutationsOf(s) <== p in AllPermutationsOf(s)
 {
@@ -207,7 +207,7 @@ lemma CorrectnessImplicationTwo<T(!new)>(s: seq<T>, p: seq<T>)
 
 An inspection of the definition of `CalculateAllPermutationsOf` shows that this means we have to construct a permutation `p'` that is in `CalculateAllPermutationsOf(s[1..])` and some index `i` of `p'` , such that `p == InsertAt(p’, s[0], i)`. How do we find `p'` and `i`? Intuitively, the idea is as follows: we define `i` as the index of the first occurrence of `s[0]` in `p` (which we know exists, since `p`, as permutation, contains the same elements as `s`) and `p'` as the sequence that one obtains when deleting the `i`-th element of `p`. To formalise this idea, we introduce the following two functions:
 
-```
+``` dafny
 function FirstOccurrence<T(==)>(p: seq<T>, x: T): (i: nat)
   requires x in multiset(p)
   ensures i < |p|
@@ -230,7 +230,7 @@ To conclude the proof, it remains to establish that i) `p' in CalculateAllPermut
 
 For i), the idea is to apply the induction hypothesis `CorrectnessImplicationTwo(s[1..], p')`, which yields the desired result if `p'` is a permutation of `s[1..]`. Since `p` was a permutation of `s`, and `p'` was obtained from `p` by deleting its first element, the statement is intuitively true. Formally, we establish it with the call  `PermutationBeforeAndAfterDeletionAt(p, s, i, 0)` to the following, slightly more general, lemma:
 
-```
+``` dafny
 lemma PermutationBeforeAndAfterDeletionAt<T>(p: seq<T>, s: seq<T>, i: nat, j: nat)
   requires IsPermutationOf(p, s)
   requires i < |p|
@@ -263,7 +263,7 @@ The proof of `PermutationBeforeAndAfterDeletionAt` is mostly a direct consequenc
 
 To establish ii), that is, the equality `p == InsertAt(p’, s[0], i)`, we recall that by construction `p' == DeleteAt(p, i)`. Substituting `p’` for its definition and using the postcondition `p[i] == s[0]` of `FirstOccurrence` thus leads us to the following lemma, which states that deleting an element of a sequence, before inserting it again at the same position, leaves the initial sequence unchanged:
 
-```
+``` dafny
 lemma InsertAfterDeleteAt<T>(s: seq<T>, i: nat)
   requires i < |s|
   ensures s == InsertAt(DeleteAt(s, i), s[i], i)