brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2024-11-25 09:36:31 -05:00
Code Issues Projects Releases Packages Wiki Activity

Update to mention common invariants

Browse source
This commit is contained in:
Brandon Rozek 2022-02-26 21:41:19 -05:00
parent fcc8c5bb1f
commit 3996e177f8
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
content/blog/dafny-loops.md
View file

@ -33,10 +33,15 @@ In order to solve this, we need to concept of a loop invariant. A loop invariant
$$ $$
\neg Loop\_Condition \wedge Loop\_Invariants \implies Post\_Condition \neg Loop\_Condition \wedge Loop\_Invariants \implies Post\_Condition
$$ $$
If this is not the case, then Dafny will likely complain to you as it has no clue what's going on. Here are the invariants you need to add in order for it to verify: If this is not the case, then Dafny will likely complain to you as it has no clue what's going on. I generally always first add bounds to the iterator and other variables.
```csharp ```csharp
invariant 0 <= i <= n invariant 0 <= i <= n
```
Here are the other invariants you'll need in order for the postcondition in the example to verify:
```csharp
invariant forall k :: 0 <= k < i ==> a[k] >= 0 invariant forall k :: 0 <= k < i ==> a[k] >= 0
invariant forall k :: 0 <= k < i ==> a[k] == k invariant forall k :: 0 <= k < i ==> a[k] == k
invariant forall j, k :: 0 <= j <= k < i ==> a[j] <= a[k] invariant forall j, k :: 0 <= j <= k < i ==> a[j] <= a[k]