An Executable Specification of C♯

Horatiu Jula, Nicu G. Fruja · Repository for Publications and Research Data (ETH Zurich) · 2005

The Abstract State Machines (ASMs) theory has been ap plied to rigorously formalize the semantics of the C] programming lan guage. The developed ASM model is validated here by providing an executable model which supports the experimentation with the ASM model. The executable model is a refinement of the ground model and is implemented in AsmL – the Abstract State Machine Language, which is embedded into Microsoft Visual Studio .NET. We report here on the development of AsmL Executable Specifications of the C] semantics by depicting our techniques on building and using AsmL as a Specification Language.

Read the paper · More papers on PaperTik