Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Finish most of part 5 of SPA series

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-11-03 16:58:06 -08:00
parent 3be67ca4c8
commit 615aeb72da
1 changed files with 68 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
content/blog/05_spa_agda_semantics/index.md
View File

@ -418,13 +418,52 @@ to evaluate the _expression_ that serves as the condition. We then had an
additional premise that requires the truthiness of the resulting value \(v\).
The rule for evaluating a conditional with a "false" branch is very similar.
{{< latex >}}
\frac
{ \rho_1 , e \Downarrow v \quad v = 0 \quad \rho_1, s_2 \Rightarrow \rho_2}
{ \rho_1, \textbf{if}\ e\ \{ s_1 \}\ \textbf{else}\ \{ s_2 \}\ \Rightarrow \rho_2 }
{{< /latex >}}
Now that we have rules for conditional statements, it will be surprisingly easy
to define the rules for `while` loops. A `while` loop will also have two rules,
one for when its condition is truthy and one for when it's falsey. However,
unlike the "false" case, a while loop will do nothing, leaving the environment
unchanged:
{{< latex >}}
\frac
{ \rho_1 , e \Downarrow v \quad v = 0 }
{ \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_1 }
{{< /latex >}}
The trickiest rule is for when the condition of a `while` loop is true.
We evaluate the body once, starting in environment \(\rho_1\) and finishing
in \(\rho_2\), but then we're not done. In fact, we have to go back to the top,
and check the condition again, starting over. As a result, we include another
premise, that tells us that evaluating the loop starting at \(\rho_2\), we
eventually end in state \(\rho_3\). This encodes the "rest of the iterations"
in addition to the one we just performed. The environment \(\rho_3\) is our
final state, so that's what we use in the rule's conclusion.
{{< latex >}}
\frac
{ \rho_1 , e \Downarrow v \quad v \neq 0 \quad \rho_1 , s \Rightarrow \rho_2 \quad \rho_2 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 }
{ \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 }
{{< /latex >}}
And that's it! We have now seen every rule that defines the little object language
I've been using for my Agda work. As with all the other rules we've seen, the
mathematical notation above can be directly translated into Agda:
{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 47 64 >}}
Below is a Bergamot widget that implements these rules. Try the following program,
which computes the `x`th power of two, and stores it in `y`:
```
x = 5; y = 1; while (x) { y = y + y; x = x - 1 }
```
{{< bergamot_widget id="stmt-widget" query="" prompt="step(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?env)" modes="Statement:Statement" >}}
hidden section "" {
Eq @ eq(?x, ?x) <-;
@ -460,3 +499,31 @@ hidden section "" {
EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y));
}
{{< /bergamot_widget >}}
### Semantics as Ground Truth
Prior to this post, we had been talking about using lattices and monotone
functions for program analysis. The key problem with using this framework to
define analyses is that there are many monotone functions that produce complete
nonsese; their output is, at best, unrelated to the program they're supposed
to analyze. We don't want to write such functions, since having incorrect
information about the programs in question is unhelpful.
What does it mean for a function to produce correct information, though?
In the context of sign analysis, it would mean that if we say a variable `x` is `+`,
then evaluating the program will leave us in a state in which `x` is posive.
The semantics we defined in this post give us the "evaluating the program piece".
They establish what the programs _actually_ do, and we can use this ground
truth when checking that our analyses are correct. In subsequent posts, I will
prove the exact property I informally stated above: __for the program analyses
we define, things they "claim" about our program will match what actually happens
when executing the program using our semantics__.
A piece of the puzzle still remains: how are we going to use the monotone
functions we've been talking so much about? We need to figure out what to feed
to our analyses before we can prove their correctness.
I have an answer to that question: we will be using _control flow graphs_ (CFGs).
These are another program representation, one that's more commonly found in
compilers. I will show what they look like in the next post. I hope to see you
there!