Skip to content
Snippets Groups Projects
Commit 9713a59f authored by David Söderberg's avatar David Söderberg
Browse files

Update HOME_EXAM.md

parent 15838008
No related branches found
No related tags found
No related merge requests found
......@@ -280,9 +280,9 @@ let b = 2;
### Operands for integer expressions
```math
\frac{<e_1,σ> → n_1 <e_2, σ> → n_2}{<e_1 - e2, σ> → n_1 \text{ minus } n_2}
\frac{<e_1,σ> → n_1 <e_2, σ> → n_2}{<e_1 - e2, σ> → n_1 \text{ sub } n_2}
```
Above is a minus operation of two integers, following integer expressions can be described in the same way:
Above is a subtraction operation of two integers, following integer expressions can be described in the same way:
- +, Addition
- *, Multiplication
- /, Division
......@@ -427,6 +427,7 @@ while a < 10 {
> - Give a simplified set of Type Checking Rules for your language (those rules look very much like the SOS rules, but over types not values). Also here you don't need to detail rules that are similar (follow the same pattern).
> - Demonstrate each "type rule" by an example. You may use one or several "programs" to showcase where rules successfully apply.
> - For your implementation, give a set of programs demonstrating that ill-typed programs are rejected, connect back to the Type Checking Rules to argue why these are illegal and thus should be rejected.
##### Symbols:
- σ, type state
......@@ -455,11 +456,16 @@ while a < 10 {
```math
\frac{<e_1,σ> → \text{i32} <e_2, σ> → \text{i32}}{<e_1 - e2, σ> → \text{i32}}
```
Above is a minus operation of two integers, these will evaluate to i32. Following operands can also be used:
Above is a subtraction operation of two integers, these will evaluate to i32. Following operands can also be used:
- +, Addition
- *, Multiplication
- /, Division
```rust
(3+5)*(4-2);
1 / false; // Type missmatch
```
### Boolean type operands
```math
\frac{<e_1,σ> → \text{bool} <e_2, σ> → \text{bool}}{<e_1 != e2, σ> → \text{bool}}
......@@ -480,6 +486,13 @@ These operands can also be used with the type i32 as follows:
\frac{<e_1,σ> → \text{i32} <e_2, σ> → \text{i32}}{<e_1 <= e2, σ> → \text{bool}}
```
```rust
true != false;
3 < 2;
false == 5; // Type missmatch
false < 2; // Type missmatch
```
### Reference and Dereference
```math
\frac{<e,σ> → \&t}{<*e,σ> → t}
......@@ -493,14 +506,95 @@ These operands can also be used with the type i32 as follows:
\frac{<*e,σ> → t}{<e,σ> → \&t}
```
```rust
let a = 0;
let b = &a;
let c = *b;
let d:bool = *b; // <-- Type missmatch
```
#### Function call
```math
\frac{<f(e_1,e_2,...,e_n),σ> → <t,σ'>; <e_1,σ> → t; ...; <e_n, σ>→ t}{<f, σ> → t}
```
``` rust
fn func() -> i32 {
1+3
}
fn main() {
let a = func();
let b:bool = a(); // Type missmatch
}
```
### Let expression
```math
\frac{<e, σ> → t, σ'}{<\text{let id} = e, σ> → σ'[\text{id} = e]}
```
``` rust
let a:i32 = 1;
let b:bool = 1; // Type missmatch
```
### Assign expression
```math
\frac{<v, σ> → \text{mut }t <e, σ> → t}{<v=t, σ>}
```
``` rust
let mut a:bool = false;
a = 0; // Type missmatch
let b:i32 = 1;
b = false; // Non mutable
```
> - For your implementation, give a set of programs demonstrating that ill-typed programs are rejected, connect back to the Type Checking Rules to argue why these are illegal and thus should be rejected.
### If true/false expression
```math
\frac{<e, σ> → bool <c_1, σ> → t <c_2, σ> → t}{<\text{if } e \text{ then }c_1 \text{ else } c_2,σ> → t}
```
``` rust
if 3 > 5 {
func();
}
else {
anotherfunc();
}
if 3 - 5 { // Type missmatch
func();
}
else {
anotherfunc();
}
```
### While expression
```math
\frac{<e, σ> → bool <c, σ> → σ'}{<\text{while } e \text{ do } c, σ> → ()}
```
```math
\frac{<b, σ> → false}{<\text{while } b \text{ do } c, σ> → σ}
```
``` rust
let a = 0;
while a < 10 {
// something that should loop 10 times
a = a + 1;
}
let a = 0;
while a * 10 { // Type missmatch
// something that should loop 10 times
a = a + 1;
}
```
> - Compare your solution to the requirements (as stated in the README.md). What are your contributions to the implementation.
Our type checker rejects bad programs according to our rules and depending on what the error is you will get a error custom message.
## Your borrrow checker
- Give a specification for well versus ill formed borrows. (What are the rules the borrow checker should check).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment