blob: e256c82cd7ad74701c7cbe757de577d4c2ccc0b9 (
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
26
|
+++
title = "Correctness argument for translation validation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a7a"]
forwardlinks = ["3a7c"]
zettelid = "3a7b"
+++
Why is translation validation correct?
If you have two languages $S$ and $T$ that you are translating in
between, you are first going to evaluate both languages using abstract
evaluation. This is a translation to a third intermediate language that
consists of a forest of registers $\mathcal{A}$.
The first step in the correctness of the translation from the input
language $S$ to $\mathcal{A}$ is semantics preserving. This can be done
because semantics have to be defined for the abstract interpretation.
Then, using the same semantics for $\mathcal{A}$, one can prove that the
translation from $T$ to $\mathcal{A}$ is also semantics preserving. Then
one can prove the following:
$$ \frac{s : S \rightarrow_s \alpha : \mathcal{A} \quad t : T \rightarrow_t\alpha' : \mathcal{A} \quad \alpha \sim \alpha'}{s \sim t} $$
|
