Executable semantics. An executable semantics is an algorithmic version of the operational semantics that allows one to compute the set of behaviors of a given program.It is generally used to reason about program transformations and to prove metatheoretical properties. Operational semantics. An operational semantics describes the behavior of programs using individual computational steps.We have, based on the C11 standard, defined the following kinds of semantics for C in Coq and proved that these correspond to each other. By developing multiple versions of the semantics, we have considered C from different perspectives and have thereby obtained a higher confidence in the correctness of our specification. ![]() Most importantly, Coq allows us to define multiple versions of the C semantics and to prove that these versions correspond to each other. Coq ensures that all definitions comprising the formal specification (the semantics) are mathematically well-formed and enjoy desirable properties. This way, one can develop reliable C programs without sacrificing the benefits of C.Īll parts of our formal specification of C are defined in the Coq proof assistant. Our formal specification of C can be used as the basis for formal verification of C programs. On the other hand, C is bug-prone due to its weak type system and the absence of run-time checks. C is widely used because of the performance of programs, the control over system resources such as memory, and the fact that C programs run on nearly any computer platform. The C programming language is addressed in this thesis because it is both among the most widely used and among the most bug-prone programming languages. ![]() Our formal specification of C, which is named CH2O, is used for the development of technology that enables verification of C programs in a standards compliant and compiler independent way. This thesis describes a formal specification of the sequential fragment of the C programming language based on the official description of the C language, the C11 standard.
0 Comments
Leave a Reply. |