Codecharts: Roadmaps and blueprints for object-oriented programs

Chapter 14

Abstract Semantics

Meaning is what an explanation of meaning explains.

—Ludwig Wittgenstein

The principle of automated verifiability (§3.4) dictates that the verification question (“does program p satisfy specification Ψ?”) must have an algorithmic answer, that is, that it can be answered by a computer program. It requires us to establish rigorously the relation between specifications and programs. We do so by offering a precise and appropriately abstract representation of object-oriented programs, an abstract semantics, which can then be fed into the verification algorithm. This chapter is concerned with such representations of programs.

Programs in object-oriented languages such as Java, C++, and C# are normally encoded and represented as text files. The collection of these files (along with some compilation information) is generally referred to as the source code. The source code is the ultimate specification of the program: It is the means by which programmers encode programs. The source code consists of the detailed set of instructions dictating how the target computer operates. By speaking of “the program” or “the implementation” we normally refer to the source code.

However, source code poses serious problems for design verification and reasoning. Source code is generally:

• Very large: consisting of many thousand (or millions) lines of code
• Decentralized: spanning hundreds of text files across a directory structure
• Complex and verbose: containing myriad implementation ...