9 November 2010
Runtime assertions in Java with the assert statement. Logical assertions in Hoare Logic, building on first-order logic and a simple imperative language; Hoare triples. Rules for derivation; validity with respect to an operational semantics; soundness and completeness. Applications in program specification and verification; tools for formal verification; Design by Contract™ and lightweight verification.
The next lecture is at 9am on Friday. Before then:
- Read the two JML articles mentioned in the lecture:
- Design by Contract with JML.
- An overview of JML tools and applications.
- Try to prove some of the example triples given in the slides using the Hoare rules and logic. This may be more intricate than you expect!
- Here are another couple of little exercises:
- Define a command C that computes the exponentiation function exp(m,n) and places the result in variable p. Give a correctness specification for it as a Hoare triple, and prove that C meets the specification.
- Devise a proof rule for an alternative loop command of the form do C while B .
- (For the techies): Try to install some of the JML tools, such as ESC/Java 2 (from Kind Software at the University of Dublin). If you succeed, please post details of what you did and some example test cases to prove it works. This is also more intricate than you might expect — installing research prototypes is sometimes a challenge. I am trying it too!
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.
- 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:
- are Java assertions a language “augmentation” or language feature?
- What about pragmas or directives available in languages like Ada, C, C++,…?
- Can you think of other examples of augmentations?
- Finally, (for the inventive): can you think of a better terminology than “augmentation”, or (for the scholars) tell us about another terminology used elsewhere?
2 November 2010
A Framework for High-Level Programming of Heterogeneous Manycore Systems-on-Chip
University of Glasgow
3.30pm Thursday, 4th November 2010
Room G.07, Informatics Forum
Links: Colloquium abstract; Institute for Computing Systems Architecture
This talk presents the Gannet framework for programming heterogeneous manycore systems-on-a-chip. This is an architecture and programming language for directly targeting such devices, rather than delegating the challenge to operating system support mechanisms like threads and tasks.
You may need to sign in to enter the Forum, but state that you are attending a research seminar, following item 3 of the Forum access policy.