We define a semantics for the arithmetic part of PASCAL by giving it

an interpretation in LCF, a language based on the typed λ-calculus.

Programs are represented in terms of their abstract syntax. We show

sample proofs, using LCF, of some general properties of PASCAL and

the correctness of some particular programs. A program implementing

the McCarthy Airline reservation system is proved correct.

In this paper we show that every flowchart program can be written

without 'go-to' statements by using 'while' statements. The main

idea is to introduce new variables to preserve the values of certain

variables at particular points in the program; or alternatively, to

introduce special boolean variables to keep information about the

course of the computation. The new programs preserve the 'topology'

of the original program, and are of the same order of efficiency. We

also show that this cannot be done in general without adding

variables.