Speaker: Gil Messerman 

Title:
Dynamic frames concept and its usage in Dafny OO programming
language.


Abstract:

When describing a computation, the specification should contain
information about what part of the state is modified and what part
remains unchanged. This can be achieved quite easily in non-modular
systems, where we know all the program variables. The difficulties
rise in modular programming, where not all the variables are known
and where we want to separate between the public and the private
state of the object. In modular systems, we need to use an abstract
specification of the object (specification variables) that
encapsulates its private state. Unfortunately, when the program
language supports pointers, such specification is not trivial, since
the private state of the object and state of the different object can
share same locations on the heap. Some solutions to this problem
introduce programming restrictions, such as limitations of object's
move across encapsulation boundaries.

 
In the talk we'll describe the frame problem for programming theories
and a concept named Dynamic Frames that provides a flexible way of
describing classes, built in layers, where one object is implemented
in terms of the other. This concept supports both the specification
variables and the pointers, without applying the programming
restrictions. Further on, we will introduce OO programming language
named Dafny that makes use of specifications based on style of
dynamic frames. We will show how to write and specify programs in
Dafny, as well as translating the program into intermediate language,
which can be further converted into input to the automatic program
verifier.