From c3c9b48b296eb8a3e4613a9f493e586fc5731b12 Mon Sep 17 00:00:00 2001 From: Mark Hakansson <marhak-6@student.ltu.se> Date: Wed, 13 Nov 2019 15:36:36 +0000 Subject: [PATCH] Update HOME_EXAM.md --- HOME_EXAM.md | 155 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 105 insertions(+), 50 deletions(-) diff --git a/HOME_EXAM.md b/HOME_EXAM.md index 22938f3..af30f68 100644 --- a/HOME_EXAM.md +++ b/HOME_EXAM.md @@ -108,102 +108,135 @@ All code has been written by me with inspiration from Per's parser example on Gi ### Structural Operational Semantics -$n \in num$ - -$b \in bool$ - -$x \in var$ - -$e \in expr$ +```math +n \in num +\\ +b \in bool +\\ +x \in var +\\ +e \in expr +``` function call (void): - -$\lang fc, \sigma \rang \Downarrow void$ +```math +\lang fc, \sigma \rang \Downarrow void +``` function call (i32): - -$\lang fc, \sigma \rang \Downarrow n$ +```math +\lang fc, \sigma \rang \Downarrow n +``` function call (bool): - -$\lang fc, \sigma \rang \Downarrow b$ +```math +\lang fc, \sigma \rang \Downarrow b +``` binomial operation (addition): - -$\frac{\lang e1,\sigma \rang \Downarrow n1 \lang e2,\sigma \rang \Downarrow n2}{\lang e1 \text{ + }e2 \rang \Downarrow n1 \text{ plus } n2}$ +```math +\frac{\lang e1,\sigma \rang \Downarrow n1 \lang e2,\sigma \rang \Downarrow n2}{\lang e1 \text{ + }e2 \rang \Downarrow n1 \text{ plus } n2} +``` left-hand side expression sequence (keywords): +```math +\frac{\lang lhs1,\sigma \rang \Downarrow \sigma' \lang lhs2,\sigma' \rang \Downarrow \sigma''}{\lang lhs1;lhs2,\sigma \rang \Downarrow \sigma''} +``` -$\frac{\lang lhs1,\sigma \rang \Downarrow \sigma' \lang lhs2,\sigma' \rang \Downarrow \sigma''}{\lang lhs1;lhs2,\sigma \rang \Downarrow \sigma''}$ let: - -$\frac{}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]}$ +```math +\frac{}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]} +``` while-false: - -$\frac{\lang b,\sigma \rang \Downarrow false}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma}$ +```math +\frac{\lang b,\sigma \rang \Downarrow false}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma} +``` while-true: - -$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while b do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma''}$ +```math +\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while b do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma''} +``` if: - -$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}$ +```math +\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'} +``` ### Explanation The example program starts from "main" and assigns the variable "a" to an i32 value returned from a function call to "test_one" with the argument "true". In the "test_one" function a variable "a" is assigned to "0": -$\frac{}{\lang a := 0,\sigma \rang \Downarrow \sigma[a := 0]}$ +```math +\frac{}{\lang a := 0,\sigma \rang \Downarrow \sigma[a := 0]} +``` then the if-statement is checked with the value "true": -$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}$ +```math +\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'} +``` this sets the value to "a" to be "50": -$\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}$ +```math +\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]} +``` then variable "a" is returned -$\lang \textit{test\_one}, \sigma \rang \Downarrow 50$ +```math +\lang \textit{test\_one}, \sigma \rang \Downarrow 50 +``` In the "main" function "a" is set to the returned value: - -$\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}$ +```math +\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]} +``` After that variable "b" is declared as an i32 value to the return value from "test_two" with the values "a", "true" and "50". In the "test_two" function variable "variable" is declared as a boolean expression. In the boolean expression the paranthesised expressions is first evaluated: -$\frac{\lang a, \sigma \rang \Downarrow 50 \lang c, \sigma \rang \Downarrow 50}{\lang \textit{a equals c}, \sigma \rang \Downarrow true}$ +```math +\frac{\lang a, \sigma \rang \Downarrow 50 \lang c, \sigma \rang \Downarrow 50}{\lang \textit{a equals c}, \sigma \rang \Downarrow true} +``` then with the rest: -$\frac{\lang \textit{a and c},\sigma \rang \Downarrow true \lang b,\sigma \rang \Downarrow true}{\lang \textit{(a equals c) and b} \rang \Downarrow true}$ +```math +\frac{\lang \textit{a and c},\sigma \rang \Downarrow true \lang b,\sigma \rang \Downarrow true}{\lang \textit{(a equals c) and b} \rang \Downarrow true} +``` Thus the variable "variable" is set to the value "true". And the variable "num" to "0". Then the while-loop starts with the condition "variable". Since "variable" is set to true the loop starts: -$\frac{\lang variable,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while variable do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while variable do block},\sigma \rang \Downarrow \sigma''}$ +```math +\frac{\lang variable,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while variable do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while variable do block},\sigma \rang \Downarrow \sigma''} +``` Inside the "block" the variable "num" is incremented by + "1" -$\frac{}{\lang num := num + 1,\sigma \rang \Downarrow \sigma[num := num + 1]}$ +```math +\frac{}{\lang num := num + 1,\sigma \rang \Downarrow \sigma[num := num + 1]} +``` and directly after "variable" is set to "false": -$\frac{}{\lang variable := false,\sigma \rang \Downarrow \sigma[variable := false]}$ +```math +\frac{}{\lang variable := false,\sigma \rang \Downarrow \sigma[variable := false]} +``` since the variable "variable" is false the while-loop will not execute the inner block and the state is unchanged: -$\frac{\lang variable,\sigma \rang \Downarrow false}{\lang \textit{while variable do block},\sigma \rang \Downarrow \sigma}$ +```math +\frac{\lang variable,\sigma \rang \Downarrow false}{\lang \textit{while variable do block},\sigma \rang \Downarrow \sigma} +``` Finally "num" is returned which has the value of "1". Back in the "main" function "b" is set to the return value of "test_two" which was "1". And then another variable "c" is declared to "a + b". Which will be "51". @@ -215,33 +248,47 @@ The current interpreter supports this SOS and can execute programs according to ### Type Checking Rules let (bool): -$\frac{\lang x,\sigma \rang \Downarrow bool \lang b,\sigma \rang \Downarrow bool}{\lang x := b,\sigma \rang \Downarrow \sigma[x := b]}$ +```math +\frac{\lang x,\sigma \rang \Downarrow bool \lang b,\sigma \rang \Downarrow bool}{\lang x := b,\sigma \rang \Downarrow \sigma[x := b]} +``` let (i32): -$\frac{\lang x,\sigma \rang \Downarrow i32 \lang n,\sigma \rang \Downarrow i32}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]}$ +```math +\frac{\lang x,\sigma \rang \Downarrow i32 \lang n,\sigma \rang \Downarrow i32}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]} +``` binomial operation (math): -$\frac{\lang expr1,\sigma \rang \Downarrow i32 \lang expr2,\sigma \rang \Downarrow i32}{\lang \textit{ expr1 math\_token }expr2 \rang \Downarrow i32}$ +```math +\frac{\lang expr1,\sigma \rang \Downarrow i32 \lang expr2,\sigma \rang \Downarrow i32}{\lang \textit{ expr1 math\_token }expr2 \rang \Downarrow i32} +``` binomial operation (boolean): -$\frac{\lang expr1,\sigma \rang \Downarrow bool \lang expr2,\sigma \rang \Downarrow bool}{\lang \textit{ expr1 bool\_token }expr2 \rang \Downarrow bool}$ +```math +\frac{\lang expr1,\sigma \rang \Downarrow bool \lang expr2,\sigma \rang \Downarrow bool}{\lang \textit{ expr1 bool\_token }expr2 \rang \Downarrow bool} +``` binomial operation (relational): -$\frac{\lang expr1,\sigma \rang \Downarrow bool \lang expr2,\sigma \rang \Downarrow bool}{\lang \textit{ expr1 relation\_token }expr2 \rang \Downarrow bool}$ +```math +\frac{\lang expr1,\sigma \rang \Downarrow bool \lang expr2,\sigma \rang \Downarrow bool}{\lang \textit{ expr1 relation\_token }expr2 \rang \Downarrow bool} +\\ -$\frac{\lang expr1,\sigma \rang \Downarrow i32 \lang expr2,\sigma \rang \Downarrow i32}{\lang \textit{ expr1 relation\_token }expr2 \rang \Downarrow bool}$ +\\ +\frac{\lang expr1,\sigma \rang \Downarrow i32 \lang expr2,\sigma \rang \Downarrow i32}{\lang \textit{ expr1 relation\_token }expr2 \rang \Downarrow bool} +``` if: - -$\frac{\lang condition,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang}$ +```math +\frac{\lang condition,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang} +``` while: - -$\frac{\lang condition,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang}$ +```math +\frac{\lang condition,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang} +``` ### Examples Let's assign a new variable that is of type "i32" to an i32 values: @@ -249,7 +296,9 @@ Let's assign a new variable that is of type "i32" to an i32 values: let a: i32 = 32; ``` The type rule is as follows: -$\frac{\lang a,\sigma \rang \Downarrow i32 \lang n,\sigma \rang \Downarrow i32}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]}$ +```math +\frac{\lang a,\sigma \rang \Downarrow i32 \lang n,\sigma \rang \Downarrow i32}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]} +``` For a relational operation such as ```rust @@ -257,7 +306,9 @@ let b: bool = 30 > 10; ``` it will follow the following type rule: -$\frac{\lang 30,\sigma \rang \Downarrow i32 \lang 10,\sigma \rang \Downarrow i32}{\lang 30 \textit{ > }10 \rang \Downarrow bool}$ +```math +\frac{\lang 30,\sigma \rang \Downarrow i32 \lang 10,\sigma \rang \Downarrow i32}{\lang 30 \textit{ > }10 \rang \Downarrow bool} +``` For an if-statement: @@ -269,7 +320,9 @@ if b { ``` which will follow the type rule: -$\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang}$ +```math +\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang} +``` For while-statements: ```rust @@ -281,7 +334,9 @@ while b { and the type rule: -$\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang}$ +```math +\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang} +``` The implemented type checker follows the rules above and should it find that there is a type mistmatch, errors will be returned. The current error implementation does not stack, only the first found error will be sent to the terminal. It does however send some information on where the error occured. -- GitLab