{true}
{A[0] = A[0] & 0=0}
m = A[0]
{m = A[0] & 0=0 & m is contained in the array}
i = 0
{m = A[0] & i=0& m is contained in the array}
{for all k<=i m<=A[k] &i=0& m is contained in the array}
do
 {for all k<=i m<=A[k] &i=0 v for all k < i m<=A[k] & i <=n& m is contained in the array}
 {for all k<i m<=A[k] & i <= n& m is contained in the array}
until i = n
 {for all k<i m<=A[k] & i<=n & i!=n& m is contained in the array}
 {for all k<i m<=A[k] & i < n& m is contained in the array}
 if m > A[i]
  {for all k<i m<=A[k] & m>A[i] & i < n& m is contained in the array}
  {for all k<=i A[i] <= A[k] & i < n& A[i] is contained in the array}
  m = A[i]
  {for all k<=i m <= A[k] & i < n & m is contained in the array}
 else
  {for all k<i m<=A[k] & m<=A[i] & i < n & m is contained in the array}
  {for all k<=i m<=A[k]& i < n & m is contained in the array}
 end if
 {for all k<=i m<=A[k]& i < n & m is contained in the array}
 {for all k<i+1 m<=A[k] & i+1 <=n& m is contained in the array}
 i = i+1
 {for all k < i m<=A[k] & i <=n& m is contained in the array}
end do
{for all k < i m<=A[k] & i <=n & i=n& m is contained in the array}
{for all k < i m<=A[k] & i=n& m is contained in the array}
{for all k < n m<=A[k]& m is contained in the array}

I know that m <= everything in the array.  But I never proved that m is itself somewhere in the array.

for some k<n m = A[k]

m = A[0]
i = 0
do
until i = n
 if m > A[i]
  m = A[i]
 else
 end if
 i = i+1
end do

The above formal verification proves that our algorithm is partially correct.  "Correct provided it terminates."

How do we prove that the loop terminates?

The technique I use is based on Well-Ordering Principle of Cardinal numbers.  "Any nonempty set of cardinal numbers has a smallest member."

The corollary is that if you start from ANY cardinal number and repeatedly choose a smaller number from what you have already chosen, you will choose zero after a FINITE number of steps.

If we have an integer flag that always gets smaller and never goes negative, the loop must terminate.  (You will get to zero in a finite number of steps.)  (And...if you have to...you can initialize the flag to be a cardinal infinity, and the idea still works.)

{true}
{A[0] = A[0] & 0=0}
m = A[0]
{m = A[0] & 0=0 & m is contained in the array}
i = 0
{m = A[0] & i=0& m is contained in the array}
{for all k<=i m<=A[k] &i=0& m is contained in the array & n=n}
ct = n
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct=n & ct>=0 & n+1=n+1}
oct = n+1
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct=n & ct>=0 & oct=n+1}
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct>=0 & ct < oct}
do
 {for all k<=i m<=A[k] &i=0 v for all k < i m<=A[k] & i <=n& m is contained in the array & ct>=0 & ct < oct}
 {for all k<i m<=A[k] & i <= n& m is contained in the array& ct>=0 & ct < oct}}
until i = n
 {for all k<i m<=A[k] & i<=n & i!=n& m is contained in the array& ct>=0 & ct < oct}}
 {for all k<i m<=A[k] & i < n& m is contained in the array& ct>=0 & ct < oct}}
 if m > A[i]
  {for all k<i m<=A[k] & m>A[i] & i < n& m is contained in the array& ct>=0 & ct < oct}}
  {for all k<=i A[i] <= A[k] & i < n& A[i] is contained in the array& ct>=0 & ct < oct}}
  m = A[i]
  {for all k<=i m <= A[k] & i < n & m is contained in the array& ct>=0 & ct < oct}}
 else
  {for all k<i m<=A[k] & m<=A[i] & i < n & m is contained in the array& ct>=0 & ct < oct}}
  {for all k<=i m<=A[k]& i < n & m is contained in the array& ct>=0 & ct < oct}
 end if
 {for all k<=i m<=A[k]& i < n & m is contained in the array& ct>=0 & ct < oct}
 {for all k<i+1 m<=A[k] & i+1 <=n& m is contained in the array& ct>=0 & ct < oct}
 i = i+1
 {for all k < i m<=A[k] & i <=n& m is contained in the array& ct>=0 & ct < oct}
 {for all k < i m<=A[k] & i <=n& m is contained in the array& oct>0}
 oct = ct
 {for all k < i m<=A[k] & i <=n& m is contained in the array& ct>0}
 ct = ct-1
end do
{for all k < i m<=A[k] & i <=n & i=n& m is contained in the array}
{for all k < i m<=A[k] & i=n& m is contained in the array}
{for all k < n m<=A[k]& m is contained in the array}