Formal semantic specification of a core object-oriented language
Thomas Bietenhader · Repository for Publications and Research Data (ETH Zurich) · 2004
In this project a formal semantic definition for a small object-oriented language is developed, in the context of formal verification of program correctness.From its inherent modular nature, its ability to support abstraction via information hiding and subtyping, the object-oriented paradigm seems predestined for efficient reuse of software components.This raises hopes to apply these advantages also on the topic of verification.Problems arising from this enterprise are discussed and an overview on the actual situation of research is given.A conclusion of this discussion is that specifications become the most critical part in modular verification.