It is, therefore, possible to extend a partially specified interpretation to a complete interpretation, without loss of verifiability, [...] This fact offers the possibility of automatic verification of programs, the programmer merely tagging entrances and one edge in each innermost loop.

p. 25 - Assigning Meanings to Programs (1967)