(Ly.Lx.y)(x)

Lz.x

Lx.((Lx.y)(x))
Lx.y

FORMAL VERIFICATION

Formal verification is using mathematical techniques to prove a program correct.

And so, within a program you would have "invariants":  logical or mathematical statements that were always true at that point of the program

Basic structures or blocks:

Assignment statement var := expr

IF-ELSE-BLOCK

if (cond)
 StuffA;
else
 StuffB;
end if

LOOP

do
 STUFFA
until (cond)
 STUFFB
end do

^^^ This is called a "mid-condition loop".  There is one common programming situation where mid-condition loops are the best way to do it.

And this is file reading.
In EVERY operating system I have EVER used in my life, the only way to detect end-of-file, is to try to read past the EOF and fail.

do
 read from file
until (no bytes read)
 process stuff from file
end do

These structures can describe any algorithm.  You can also do stuff with methods and recursion; these are parts of formal verification (but we probably won't get into that).

From formal verification, we get terms like "partial correctness" and "total correctness".

"Partial correctness" means that the program gives the correct answer upon termination.

"Total correctness" means that the program is partially correct AND that it is guaranteed to terminate.

ct = 1;
do
until ct == 0
 j = 1
 ct = 0
 do
 until j=i
  if prime(i) & prime(j-i)
   ct = ct+1
  else
  endif
  j = j+1
 end do
 i = i+2
end do