A myth in the modular specification of programs
K. Rustan M. Leino · 1996
When writing specifications of modular programs, two crucial elements are abstraction and clauses. Without abstraction, information hiding is not possible; without clauses, a specification must mention the variables that go unchanged explicitly, and doing so is prohibited because most of the variables are not in scope. Reasoning about modular specifications involves the difficult area of interpreting modifies clauses in the presence of abstraction. Such interpretation should be sound, meaning that program properties that are provable hold in every execution of the program. Focusing on a commonly-thought-of-as-correct implementation of a given specification, I challenge the existence of a sound and reasonable methodology for proving such implementations correct, suggesting the legality of such implementations to be but a myth.