A Formal Semantics for C++

Select |




Print


Norrish, Michael

Norrish, Michael


2007-11-09


Report


Canberra


This document describes a formal operational model of the dynamic semantics of much of the C++ language (as specified in the ISO Standard). The formal model was developed in the HOL theorem-prover, providing additional guarantees as to its good sense. This report presents and explains extracts from the mechanised source-code that was fed to HOL. This work was performed under funding from QinetiQ’s Systems Assurance Group under the UK MOD Output 3a research project entitled Robust Languages.


nicta:1203


Norrish, Michael. A Formal Semantics for C++. 2007-11-09. nicta:1203.



Loading citation data...

Citation counts
(Requires subscription to view)