Sequential programming

flowchart TD

1[x>=0] --> 2[z+u*y = x*y & u >=0] --> 4[z = x*y]

Annotations and correctness

{P} S {Q}

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

direction LR

P --> Q: S

rules for correctness

If $P\wedge B\to Q$

Sequential composition

Array as a partial function

x := (x; E:F)

array is a function $D\to 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 )}