{P} S {Q}

---
title: correctness assertion
---
stateDiagram-v2

direction LR

P --> Q: S

Array as a partial function

x := (x; E:F)

array is a function $D \rightarrow T$ where $D$ is a ‘small’ range of integers and $T$ is the type of array element

alter function (x; E:F) is defined by

 
(x; E:F)(G) = F if E = G
(x; E:F)(G) = x(G) if e != G

For example:

Given array x:

{x(0) = a ^ x(1) = b}
x(1) := c
{x(0) = a ^ x(1) = c}

S is the sum(0..k) → loop invariant

s, k := a(0), 1`
{s = (\sum )}