blob: eaeacc32693709c859afca25eadaa04d4caaa8cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
+++
title = "Proofs "
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a4"]
forwardlinks = ["3a6", "3a5a"]
zettelid = "3a5"
+++
Assuming that there are semantics for the source program S and the
compiled program C, these semantics associate a behaviour to the
execution of the program, which can be behaviours like termination,
divergence or "going wrong" when undefined behaviour is executed.
There are several ways this proof could be done, the relationships
between them is shown below.
![][1]
In the diagram above shows the relationships between different kinds of
proofs that could be used to prove different properties about the
compiler between the source language and the compiled output.
[1]: attachment:simulations.png
|
