diff options
Diffstat (limited to 'content/zettel/3a8g5c.md')
| -rw-r--r-- | content/zettel/3a8g5c.md | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/content/zettel/3a8g5c.md b/content/zettel/3a8g5c.md new file mode 100644 index 0000000..722f8d5 --- /dev/null +++ b/content/zettel/3a8g5c.md @@ -0,0 +1,39 @@ ++++ +title = "Semantic invariance property" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a8g5b"] +forwardlinks = ["3a8e", "3a8g5d", "3a8g5c1"] +zettelid = "3a8g5c" ++++ + +A semantic invariance property needs to be found, which can be proven to +be true at any point in the graph. This then makes it easier to prove +the correctness of the predicates, as the semantic property can be used +instead if all the preconditions are met. + +The other benefit is that this property can be proven by induction on +the semantics themselves, which means that one can assume that it is +true for the previous state, and prove that it still holds for the next +state. Afterwards, one also needs to prove that it holds for the initial +state of the semantics, just like how the equations lemma was proven +([\#3a8e]). + +The invariance property that needs to be proven for the correctness +proof between the predicates and the path expressions is the following: + +```{=latex} +\begin{align} +\forall p_c\ r_s\ &m,\\ +(\forall d\ &R_{d\ \rightarrow p_c}\ P,\\ +&(\forall p, \text{path}\ d\ p\ p_c \implies + p \in \sigma(R_{d \rightarrow p_c}))\\ +&\implies t\ R_{d\ \rightarrow p_c}\ P \\ +&\implies \text{sdom}\ d\ p_c \\ +&\implies P \Downarrow (r_s, m) = T)\\ +\implies &\text{path_prop}\ p_c\ r_s\ m +\end{align} +``` + + [\#3a8e]: /zettel/3a8e |