An executable specification of C

Abstract. 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