A Floyd-like semantics is presented for the assignment statement in a fragment of ALGOL 68. The fragment considered contains array identifiers, referencing, dereferencing and conditionals. The semantics is based upon an interpretation in a model of intensional logic, without use of addresses or stores. In doing so, several ideas developed by R. Montague concerning the treatment of semantics for natural languages are applied for the first time in the area of semantics of programming languages. We also consider an operational semantics, based on the same model and prove that the Floyd-like semantics is valid with respect to the operational one and always yields the strongest postcondition.

European Conference on Numerical Mathematics and Advanced Applications
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Janssen, T.M.V, & van Emde Boas, P. (1977). On the proper treatment or referencing, dereferencing and assignment. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 282–300). doi:10.1007/3-540-08342-1_22