Lecture 12: Language Augmentations and Correctness

5 November 2010

The idea of a language “augmentation” as being an additional programming language element which contributes information about a program without changing its meaning. Augmentations might be used by the compiler or other tools to check properties, for example, correctness conditions.

Notions of correctness: verification at different levels (design, specification, implementation) and horizontal/vertical translations (refinement, optimisation, compilation). Forms of certification and example approaches: proof-carrying code, translation validation and compiler correctness.

I mentioned some example research projects which have (hopefully!) working demos.

Links: Slides; research projects: MRG, Mobius, Compcert.

Homework

  • Read more about the MRG project, and try to understand the demos. What happens when you adjust the various bits of PCC input?
  • Before next lecture: do the homework on the last slide of the lecture, namely, review predicate calculus as a preparation for Hoare Logic and follow the Java assertions tutorial to understand runtime assertion checking.
  • To discuss in the comments:
    1. are Java assertions a language “augmentation” or language feature?
    2. What about pragmas or directives available in languages like Ada, C, C++,…?
    3. Can you think of other examples of augmentations?
    4. Finally, (for the inventive): can you think of a better terminology than “augmentation”, or (for the scholars) tell us about another terminology used elsewhere?