diff options
Diffstat (limited to 'content/zettel/3a4a.md')
| -rw-r--r-- | content/zettel/3a4a.md | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3a4a.md b/content/zettel/3a4a.md new file mode 100644 index 0000000..2907812 --- /dev/null +++ b/content/zettel/3a4a.md @@ -0,0 +1,27 @@ ++++ +title = "Adding a new CompCert pass" +date = "2020-12-10" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a4"] +forwardlinks = ["3a4b"] +zettelid = "3a4a" ++++ + +The main stages that are necessary when adding a compiler pass in +CompCert are the following: + +- Specify the operational semantics and syntax of the language. +- Create the specification of the translation algorithm. +- Create the algorithm that corresponds to the specification. +- Prove that the algorithm implements the specification. +- Prove that the specification retains the behaviour of the program + according to the operational semantics of the original language and + the target language. + +These steps are all necessary when specifying complex translations, +however, when proving a simple transformation, it may not always be +necessary to provide a specification of the translation algorithm. +Instead, it is simple enough, the algorithm itself can be used for the +proof. |