blob: 37938dec873f4af0fdc10356c312c3f3c9d84341 (
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
27
28
29
30
31
|
+++
title = "Proving correctness by reducing to correctness of paths"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5d", "3a8g5a"]
forwardlinks = ["3a8e", "3a8g5c"]
zettelid = "3a8g5b"
+++
The problem of correctness of path expressions can therefore be reduced
to the correctness of paths themselves, using the following theorem (if
it can be proven):
```{=latex}
\begin{align}
\forall a\ &b\ P\ P'\ R\ s,\ \exists p,\\
&\textit{path}\ a\ p\ b \\
&\implies t_p\ p\ P \\
&\implies t\ R_{a \rightarrow b}\ P' \\
&\implies P \Downarrow s = T \\
&\implies P' \Downarrow s = T
\end{align}
```
This therefore reduces the proof to a proof that there is at least one
path that convert to a predicate which will then finally evaluate to
true. This property is therefore useful to prove the induction of the
semantics of SSA to prove the proper invariant, similar to the equations
Lemma ([\#3a8e]).
[\#3a8e]: /zettel/3a8e
|
