1.Factorial

{N ≥ 0 } // precondition
{1==1} // by consequence rule
{1 == product(int k in(1..1); k} // by assign and compose and maths
int x = 1;
{x == product(int k in(1..0+1); k} // by assign and compose
int i = 0;
{x== product (int k in (1..i+1); k} // invariant
while (i != N)
	{x == product (int k in (1..i+1); k} ^ i!=N} // Invariant and guard
	{x*(i+1)== product(int k int(1..i+1); k} // by assign and compose
i = i + 1
{x*i == product(int k in(1..i); k} //by assign
x = x * i;
{x == product (int k in (1..i); k} // invariant
{x == product {int k in (1..i); k} ^ N==i} //invariant and not(guard)
{x == product {int k in (1..N); k}} // postcondition