Toot

Written by Per Vognsen on 2024-12-30 at 09:46

@zwarich Just wrote this example, you can see how relatively low the mark-up burden is for something classical like this.

method Squares(a: array)

modifies a

ensures forall i :: 0 <= i < a.Length ==> a[i] == i * i

{

var jj, djj := 0, 1;

for j := 0 to a.Length

invariant forall i :: 0 <= i < j ==> a[i] == i * i

invariant jj == j * j && djj == 2 * j + 1

{

a[j], jj, djj := jj, jj + djj, djj + 2;

}

}

=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social

Mentions

=> View zwarich@hachyderm.io profile

Tags