Skip to content
Snippets Groups Projects
Commit b9d72170 authored by Wilma Krutrök's avatar Wilma Krutrök
Browse files

Finnished semantics part

parent 07578f9e
No related branches found
No related tags found
No related merge requests found
......@@ -255,7 +255,7 @@ The following program will be accepted by the parser.
```
#### Illeagal examples
Three examples that will be rejected by the compiler:
Three examples that will not go through the parser and be rejected by the compiler:
```rust
fn a(x: bool, y: bool) {
x || y
......@@ -311,10 +311,128 @@ In the future could the following things be implemented to allow the parser to a
- Global assignments
- Shadowing
- Pretty printing
- Mutable arguments
Currently it is needed to seperate statements with ";" (except for the last one) for the parser to interpret it as a vector. This would be nice to rewrite in the future.
## Semantics
Below is the Structural Operational Semantics (SOS) described using small-step semantics for the implemented language.
- σ, Store
- σ' and σ'', Changed store
- n, Integer
- b, Boolean
- e, Expression
- c, Commands
- x, Variable
##### Constant
```math
\frac{}{<n,σ> → n}
```
##### Variable
```math
\frac{}{<x,σ> → σ(x)}
```
##### Arithmetic, boolean & comparison operations
```math
\frac{<e0,σ> → n0 <e1,σ> → n1}{<e0 + e1,σ> → n}, \text{ where } n = n0 + n1
```
SOS for addition between two expressions.
Similar SOS goes for the following operands:
- "-", subtraction
- "*", multiplication
- "/", division
- ">", greater
- "<", less
- ">=", greater or equal
- "<=", less or equal
- "==", equals
- "!=", not equals
Can also be combined in a derivation tree.
```rust
1 - 5 + 3 * 4 / 2;
3 <= 5;
```
##### Assignment
```math
\frac{<e,σ> → e'}{<x:=e,σ> → <x:=e',σ>}
```
Let statements works in a similiar way.
```rust
let mut x: bool = true;
x = false;
```
##### Command sequence
```math
\frac{<c0,σ> → σ'' <c1,σ''> → σ'}{<c0;c1,σ> → σ'}
```
```rust
let x: i32 = 5;
x > 2;
```
##### Command conditional
```math
\frac{<b,σ> → \text{ true } <c0,σ> → σ'}{<\text{ if } b \text{ then } c0 \text{ else } c1,σ> → σ'};
```
```math
\frac{<b,σ> → \text{ false } <c1,σ> → σ'}{<\text{ if } b \text{ then } c0 \text{ else } c1,σ> → σ'}
```
```rust
if x != y {
x = x + 1;
} else {
x = x - 1;
}
```
##### Command while
```math
\frac{<b,σ> → \text{ false }}{<\text{ while } b \text{ do } c,σ> → σ};
```
```math
\frac{<b,σ> → \text{ true } <c,σ> → σ'' <\text{ while } b \text{ do } c,σ''> → σ'}{<\text{ while } b \text{ do } c,σ> → σ'}
```
```rust
while x != y {
x = x - 1;
}
```
#### Showcase step by step
When looking at the showcase and the SOS for the langugage can it be seen that the program will be executed in sequence. First will the value true be assigned to the variable start followed by a functioncall to test2(). Before executing test2() need the argument expression be evaluated and get the value true as seen in the first SOS and assign it to the variable x. In the scope for test2() will the variables a and b also be assigned followed by a functionfall to test1(). In test1() is a if then else introduced and following the SOS above does this return in true and the next if is evalueted which also is true. From here will a return statement be evalueted and the value 7 will be returned back to test2() and assign to variable c. Continuing in the method test2() will a while loop be started and because the expression is true will the block be evalueted as seen in the SOS for while. This will be repeted two more times before the expression becomes false and the state does not change. Finally is the value for variable b returned back to the main method.
#### Coverage
The following bullet points are covered by the interpreter.
- Expressions (Arithmetic, boolean, comparison)
- Let statements (Let and mutable let)
- Assignments (For mutable variables in the right scope)
- If and else
- While
- Functioncalls (With return value)
For the interpreter to accept a program is a main() method needed.
#### Future improvements
- Shadowing
- Global variables
- Better handeling of scopes
Currently the interpreter does not handle the right scopes compleatly but this is not a problem due to the type checker taking care of it.
## Type checker
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment