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