Lecture 13: Assertions and Hoare Logic

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.

Link: Slides

Homework

The next lecture is at 9am on Friday. Before then:

  1. Read the two JML articles mentioned in the lecture:
    1. Design by Contract with JML.
    2. An overview of JML tools and applications.
  2. 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!
  3. Here are another couple of little exercises:
    1. 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.
    2. Devise a proof rule for an alternative loop command of the form do C while B .
  4. (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!

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?

Lecture 11: Heterogeneous Metaprogramming in F#

2 November 2010

This is the last of three lectures on integrating domain-specific languages with general-purpose programming languages. This lecture looked at metaprogramming, where one program manipulates another; in particular the possibilities for heterogeneous metaprogramming provided by the LINQ framework mentioned in the previous lecture. This leads to an example from the following paper where existing F# code for running Conway’s Game of Life can be automatically transformed to run on a GPU.

D. Syme Leveraging .NET meta-programming components from F#: Integrated queries and interoperable heterogeneous execution. In ML ’06: Proceedings of the ACM SIGPLAN 2006 Workshop on ML, pages 43–54. ACM Press, September 2006. DOI 10.1145/1159876.1159884

Link: Slides

Coursework office hour

If you have questions or problems you wish to raise regarding the course or your coursework, you can bring them to me this Wednesday afternoon.

Office Hour: 1.30–2.30pm Wednesday 27 October, Informatics Forum 5.04

If the turnstile gates are closed and your student card does not open them, ask at the front desk for admission.

Otherwise, please post any questions here on the blog or by email either to the mailing list apl-students@inf.ed.ac.uk or to me Ian.Stark@ed.ac.uk.


ICSA Colloquium

2 November 2010

A Framework for High-Level Programming of Heterogeneous Manycore Systems-on-Chip

Wim Vanderbauwhede
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.