```sorted : Array of T  -> Bool
sorted s ==
(!i,j | i<j /\ j<#s . s[i] <= s[j] )
```
```sorted : Array of T -> (Nat->Bool) -> Bool
sorted s r ==
(!i | r i . i<#s) /\
(!i,j | r i /\ r j /\ i<j /\ j<#s . s[i] <= s[j] )
```
```     PROCEDURE Sort(s:Array of T)
s:=s' | sorted s'  /\  perm S s'    <--
```
```     CON S | S=s .
{ s=S }  s:=s' | sorted s'  /\  perm S s'        <--
```
```     VAR k .  k:=0 ;
{ k=0 /\ s=S }  s,k:=s',k' | sorted s'  /\  perm S s'        <--
```
```     DO G ->
{ INV /\ G }
s,k:=s',k' | INV'  /\  V'<V
OD
```
```     |-  k=0 /\ s=S  ==>  INV
|-  INV /\ ~G   ==>  sorted s  /\  perm S s
```
```     INV  ==  k <= #s  /\  sorted s {i|i<k}  /\  perm S s
G  ==  k < #s
V  =   #s - k
```
```     DO k < #s ->
{ k < #s  /\  sorted s {i|i<k}  /\  perm S s }     <--
s,k:=s',k' |  k' <= #s'  /\  sorted s' {i|i<k'}    <--
/\  perm S s'  /\  #s'-k' < #s-k                  <--
OD
```
```     { k < #s  /\  sorted s {i|i<k}  /\  perm S s }
s:=s' |  (k+1) <= #s'  /\  sorted s' {i|i<(k+1)}
/\  perm S s'  /\  #s'-(k+1) < #s-k ;
k:=k+1
```
```     |-  perm S s  /\  perm S s'  ==>  #s = #s'
```
```         #s'-(k+1)  <  #s-k
==  #s-(k+1)  <  #s-k          since  #s = #s'
==  #s-k-1  <  #s-k
==  true
```
```     { k < #s  /\  sorted s {i|i<k}  /\  perm S s }
s:=s' |  (k+1) <= #s'  /\  sorted s' {i|i<(k+1)}  /\  perm S s'
```
```     VAR m:Nat . m:=k;
{ k < #s  /\  sorted s {i|i<k}  /\  perm S s  /\  m=k }
s,m:=s',m' |  (k+1) <= #s'  /\  sorted s' {i|i<(k+1)}  /\  perm S s'
```
```     INV  ==  m<=k  /\  sorted s {i| i<m \/ m<i<=k } /\
( m<k ==> s[m] < s[m+1] )  /\  perm S s
G  ==  m > 0  /\  s[m-1] > s[m]
V  =   m
```
```     DO m > 0  /\  s[m] < s[m-1] ->
{ INV  /\  m > 0  /\  s[m] < s[m-1]  }
s,m:=s',m' | INV'  /\  m'<m
OD
```
```     { INV  /\  m > 0  /\  s[m] < s[m-1]  }
s:=s' |  m-1<=k  /\  sorted s' {i| i<m-1 \/ m-1<i<=k }  /\
( m-1<k ==> s'[m-1] < s'[m] )  /\  perm S s'   ;
m:=m-1
```
```     { INV  /\  m > 0  /\  s[m] < s[m-1]  }
s:=s' |  sorted s' {i| i<m-1 \/ m-1<i<=k }  /\
s'[m-1] < s'[m]  /\  perm S s'
```
```     |-  INV  /\  m > 0  /\  s[m] < s[m-1]  /\  s' = swap s m-1 m
==>  sorted s' {i| i<m-1 \/ m-1<i<=k }  /\
s'[m-1] < s'[m]  /\
perm S s'
```
```     s:=s' |  s' = swap s m-1 m
```
```     s[m-1], s[m] := s[m], s[m-1]
```
```     PROCEDURE Sort(s:Array of T)
CON S:Array of T | S=s .
VAR k:Nat .  k:=0 ;
DO k < #s ->
VAR m:Nat . m:=k;
DO m > 0  /\  s[m] < s[m-1] ->
s[m-1], s[m] := s[m], s[m-1];
m := m-1
OD;
k:=k+1
OD
```
```     PROCEDURE Sort(s:Array of T)
VAR k,m:Nat .  k:=0 ;
DO k < #s ->
m:=k;
DO m > 0  /\  s[m] < s[m-1] ->
s[m-1], s[m] := s[m], s[m-1];
m := m-1
OD;
k:=k+1
OD
```