B Theories for Ergo

Speaker: Peter Robinson

When: 10:00, Thursday, 11 March, 2004

Venue: 78-420

Abstract: The aim of this seminar is to report on the work I have been doing on
supporting the B specification language in Ergo and to get feedback
on some ideas for a theory about B machines.

I will give an overview of the theories for B sets (including relations,
functions and sequences) and show how these theories deal with undefinedness.
Because of the treatment of undefinedness the semantics of these Ergo theories
differs slightly form the semantics given in The B-Book.

More controversially, I will briefly discuss ideas for a B machine theory
whose semantics differs much more from that of The B-Book. I hope this will
spark some interesting discussion.
 

Hospitality: Speaker (by default)

Contact: Prof Paul Bailes (SSE seminar co-ordinator) (p.bailes@epsa.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html