Skip to content

Commit b798916

Browse files
Petar MaksimovicPetar Maksimovic
Petar Maksimovic
authored and
Petar Maksimovic
committed
update
1 parent 269f735 commit b798916

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+1191
-677
lines changed

‎01-calc/README.md

+61
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
# Example 1: Calculator
2+
3+
Our first example is that of a calculator that works with simple integer arithmetic, that is, addition, subtraction, multiplication, division, and exponentiation, and the first step is to define the appropriate syntax. This can be done in `K` as follows:
4+
5+
```k
6+
// Calculator syntax
7+
module CALC-SYNTAX
8+
imports INT-SYNTAX // Int is the K built-in integer sort
9+
10+
// Integer arithmetic syntax
11+
syntax Int ::=
12+
"(" Int ")" [bracket]
13+
> left: // left: indicates left associativity
14+
Int "^" Int [function] // and > indicates lower priority of below productions
15+
> left:
16+
Int "*" Int [function]
17+
| Int "/" Int [function]
18+
> left:
19+
Int "+" Int [function]
20+
| Int "-" Int [function]
21+
endmodule
22+
```
23+
24+
The next step is to define the calculator semantics by providing the set of appropriate rewriting rules of the format `[LHS] => [RHS]`, as follows:
25+
26+
```k
27+
// Calculator semantics
28+
module CALC
29+
imports INT
30+
imports CALC-SYNTAX
31+
32+
// Integer arithmetic semantics
33+
rule E1 + E2 => E1 +Int E2
34+
rule E1 - E2 => E1 -Int E2
35+
rule E1 * E2 => E1 *Int E2
36+
rule E1 / E2 => E1 /Int E2
37+
rule E1 ^ E2 => E1 ^Int E2
38+
endmodule
39+
```
40+
41+
`K` applies these rewriting rules, informally, by matching the `[LHS]` to the current expression and then rewriting that matched part to `[RHS]`. For example, `1 + 2` matches `E1 + E2` syntactically (with `1` matching `E1`, `+` matching `+` and `2` matching `E2`), which then, by the first rule, is rewritten to `1 +Int 2`, and then further evaluated via semantic integer addition to `3`.
42+
43+
## Compiling and running the calculator
44+
45+
Follow the instructions from the top-level [`README`](../README.md) file to compile the calculator and run the first test. This yields the following output:
46+
47+
```
48+
Input
49+
=====
50+
1 + 2 + 3
51+
52+
Output
53+
======
54+
<k>
55+
6 ~> .
56+
</k>
57+
```
58+
59+
which you can interpret, ignoring the `<k> ... <./k>` wrapper and the `~> .` in the `Output` portion, as "the expression `1 + 2 + 3` was successfully evaluated/rewritten to `6`".
60+
61+
You can experiment with modifying the tests, but also with modifying operator associativity and priority: for example, running `1.calc` with `+` not declared as left-associative (that is, `> Int "+" Int [function]` or `2.calc` with all operators being of the same priority (using `|` instead of `>`), both of which should result in parsing ambiguity errors. You would then have to use parentheses to manually disambiguate the parsing.

‎01-calc/calc.k

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
// Calculator syntax
2+
module CALC-SYNTAX
3+
imports INT-SYNTAX // Int is the K built-in integer sort
4+
5+
// Integer arithmetic syntax
6+
syntax Int ::=
7+
"(" Int ")" [bracket]
8+
> left: // left: indicates left associativity
9+
Int "^" Int [function] // and > indicates lower priority of below productions
10+
> left:
11+
Int "*" Int [function]
12+
| Int "/" Int [function]
13+
> left:
14+
Int "+" Int [function]
15+
| Int "-" Int [function]
16+
endmodule
17+
18+
// Calculator semantics
19+
module CALC
20+
imports INT
21+
imports CALC-SYNTAX
22+
23+
// Calculator semantics
24+
rule E1 + E2 => E1 +Int E2
25+
rule E1 - E2 => E1 -Int E2
26+
rule E1 * E2 => E1 *Int E2
27+
rule E1 / E2 => E1 /Int E2
28+
rule E1 ^ E2 => E1 ^Int E2
29+
endmodule

‎01_calc.k.sol

-22
This file was deleted.

‎02-calc-bool/README.md

+63
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
# Example 2: Calculator with Boolean Expressions
2+
3+
In this exercise, we extend the calculator of Exercise 1 to include Boolean expressions, such as the standard propositional connectives and integer comparisons. The syntax extension is straightforward, introducing the `Bool` built-in sort for Booleans, and defining top-level expressions as either integers or Booleans:
4+
5+
```k
6+
// Expression calculator syntax
7+
module CALC-BOOL-SYNTAX
8+
imports INT-SYNTAX // Int is the K built-in integer sort
9+
imports BOOL-SYNTAX // Bool is the K built-in Boolean sort
10+
11+
// Expressions are either integers or Booleans
12+
syntax Exp ::= Int | Bool
13+
14+
// Integer arithmetic syntax from Exercise 1
15+
syntax Int ::=
16+
...
17+
18+
// Integer comparison syntax
19+
syntax Bool ::=
20+
"(" Bool ")" [bracket]
21+
| Int "<=" Int [function]
22+
| Int "<" Int [function]
23+
| Int ">=" Int [function]
24+
| Int ">" Int [function]
25+
| Int "==" Int [function]
26+
| Int "!=" Int [function]
27+
28+
// Propositional connective syntax
29+
syntax Bool ::=
30+
Bool "&&" Bool [function]
31+
| Bool "||" Bool [function]
32+
endmodule
33+
```
34+
35+
The semantics is also straightforwardly extended to the newly defined operators:
36+
37+
```k
38+
// Expression calculator semantics
39+
module CALC-BOOL
40+
imports INT
41+
imports BOOL
42+
imports CALC-BOOL-SYNTAX
43+
44+
// Integer arithmetic semantics
45+
...
46+
47+
// Integer comparison semantics
48+
rule I1 <= I2 => I1 <=Int I2
49+
rule I1 < I2 => I1 <Int I2
50+
rule I1 >= I2 => I1 >=Int I2
51+
rule I1 > I2 => I1 >Int I2
52+
rule I1 == I2 => I1 ==Int I2
53+
rule I1 != I2 => I1 =/=Int I2
54+
55+
// Propositional connective semantics
56+
rule B1 && B2 => B1 andBool B2
57+
rule B1 || B2 => B1 orBool B2
58+
endmodule
59+
```
60+
61+
## Compiling and running the expression calculator
62+
63+
Follow the instructions from the top-level [`README`](../README.md) file to compile the expression calculator and run the provided tests. Create some further examples to check if they yield expected results.

‎02-calc-bool/calc-bool.k

+62
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
// Expression calculator syntax
2+
module CALC-BOOL-SYNTAX
3+
imports INT-SYNTAX // Int is the K built-in integer sort
4+
imports BOOL-SYNTAX // Bool is the K built-in Boolean sort
5+
6+
// Expressions are either integers or Booleans
7+
syntax Exp ::= Int | Bool
8+
9+
// Integer arithmetic syntax
10+
syntax Int ::=
11+
"(" Int ")" [bracket]
12+
> left: // left: indicates left associativity
13+
Int "^" Int [function] // and > indicates lower priority of below productions
14+
> left:
15+
Int "*" Int [function]
16+
| Int "/" Int [function]
17+
> left:
18+
Int "+" Int [function]
19+
| Int "-" Int [function]
20+
21+
// Integer comparison syntax
22+
syntax Bool ::=
23+
"(" Bool ")" [bracket]
24+
| Int "<=" Int [function]
25+
| Int "<" Int [function]
26+
| Int ">=" Int [function]
27+
| Int ">" Int [function]
28+
| Int "==" Int [function]
29+
| Int "!=" Int [function]
30+
31+
// Propositional connective syntax
32+
syntax Bool ::=
33+
left:
34+
Bool "&&" Bool [function]
35+
| Bool "||" Bool [function]
36+
endmodule
37+
38+
// Expression calculator semantics
39+
module CALC-BOOL
40+
imports INT
41+
imports BOOL
42+
imports CALC-BOOL-SYNTAX
43+
44+
// Integer arithmetic semantics
45+
rule I1 + I2 => I1 +Int I2
46+
rule I1 - I2 => I1 -Int I2
47+
rule I1 * I2 => I1 *Int I2
48+
rule I1 / I2 => I1 /Int I2
49+
rule I1 ^ I2 => I1 ^Int I2
50+
51+
// Integer comparison semantics
52+
rule I1 <= I2 => I1 <=Int I2
53+
rule I1 < I2 => I1 <Int I2
54+
rule I1 >= I2 => I1 >=Int I2
55+
rule I1 > I2 => I1 >Int I2
56+
rule I1 == I2 => I1 ==Int I2
57+
rule I1 != I2 => I1 =/=Int I2
58+
59+
// Propositional connective semantics
60+
rule B1 && B2 => B1 andBool B2
61+
rule B1 || B2 => B1 orBool B2
62+
endmodule

‎02_calc-bool.k.sol

-46
This file was deleted.

‎03-subst/README.md

+101
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
# Example 3: Variables in Expressions, Explicit Substitution
2+
3+
In this exercise, we take the expression calculator of the [previous exercise](../02-calc-bool/README.md) and extend the syntax of integer expressions with variables. To evaluate such expressions, we move from the functional to the stateful fragment of K, using configurations to model a variable store (hard-coded for this example), and evaluate expressions using explicit substitution. In the syntax, variables are modelled using the `K` built-in `Id` sort, and the integer and Boolean expressions contain all of the previously seen operators:
4+
5+
```k
6+
module SUBST-SYNTAX
7+
imports INT-SYNTAX // Int is the K built-in integer sort
8+
imports BOOL-SYNTAX // Bool is the K built-in Boolean sort
9+
imports ID // Id is the K built-in sort for identifiers (variables)
10+
11+
// Expressions are either integer or Boolean expressions
12+
syntax Exp ::= IExp | BExp
13+
14+
// An integer expression is either an integer value or a variable identifier
15+
syntax IExp ::= Int | Id
16+
// or any of the arithmetic operators
17+
syntax IExp ::= IExp "^" IExp
18+
> IExp "*" IExp
19+
| IExp "/" IExp
20+
> IExp "+" IExp
21+
| IExp "-" IExp
22+
// or a bracketed integer expression
23+
syntax IExp ::= "(" IExp ")" [bracket]
24+
25+
// A Boolean expression is either a Boolean value
26+
syntax BExp ::= Bool
27+
// or any of the comparison operators
28+
syntax BExp ::= IExp "<=" IExp
29+
| IExp "<" IExp
30+
| IExp ">=" IExp
31+
| IExp ">" IExp
32+
| IExp "==" IExp
33+
| IExp "!=" IExp
34+
// or any of the propositional connectives
35+
syntax BExp ::= BExp "&&" BExp
36+
| BExp "||" BExp
37+
// or a bracketed Boolean expression
38+
syntax BExp ::= "(" BExp ")" [bracket]
39+
endmodule
40+
```
41+
42+
The semantics, on the other hand, becomes more involved. First, we have to model the variable store, which we do using `K` configurations. In particular, our configuration is of the form:
43+
44+
```k
45+
configuration
46+
// K cell, containing the expression to be evaluated
47+
<k> $PGM:Exp </k>
48+
// Variable store, modelled as a K map
49+
<store>
50+
#token("a", "Id") |-> 16
51+
#token("b", "Id") |-> 9
52+
#token("c", "Id") |-> 4
53+
#token("d", "Id") |-> 2
54+
</store>
55+
```
56+
57+
and contains two components. The first is a `K` cell, which contains the expression to be evaluated and which is initially populated with the contents of the passed input file (denoted by `$PGM`). The second is the variable store, which is modelled as a `K` map, and which contains some hard-coded variables (`a`, `b`, `c`, and `d`) with their values.
58+
59+
Next, we declare that expressions should be evaluated, with each type of expressions having its dedicated substitution (`substI` and `substB`):
60+
61+
```k
62+
// Integer expression evaluation via explicit substitution
63+
rule
64+
<k> IE:IExp => substI(IE, STORE) ... </k>
65+
<store> STORE </store>
66+
requires notBool isInt(IE)
67+
68+
// Boolean expression evaluation via explicit substitution
69+
rule
70+
<k> BE:BExp => substB(BE, STORE) ... </k>
71+
<store> STORE </store>
72+
requires notBool isBool(BE)
73+
```
74+
75+
The first rule states that, given a configuration containing an integer expression `IE` and store `STORE`, if `IE` is not an integer value, then it should be rewritten to the result of the substitution given on the right hand side, and the store should remain the same. The second rule is analogous. The side conditions, given by the `requires` clauses, are there to ensure that the evaluation terminates.[^1]
76+
77+
The actual integer substitution function is defined as follows (with some non-instructive cases elided):
78+
79+
```k
80+
// Integer expression substitution
81+
syntax Int ::= substI ( IExp , Map ) [function]
82+
83+
// Base case: integer values evaluate to themselves
84+
rule substI(I:Int, _SUBST) => I
85+
86+
// Base case: identifiers evaluate to their value in the store
87+
rule substI(I:Id, SUBST) => {SUBST [ I ]}:>Int
88+
89+
// Inductive cases
90+
rule substI(I1 + I2, SUBST) => substI(I1, SUBST) +Int substI(I2, SUBST)
91+
rule substI(I1 - I2, SUBST) => substI(I1, SUBST) -Int substI(I2, SUBST)
92+
...
93+
```
94+
95+
The substitution is defined as a function mapping an integer expression (`IExp`) and a variable store (`Map`) to an integer. It has two base cases, which state that integers evaluate to themselves, and that variables evaluate to their value in the store (denoted by `[SUBST [I]]`). The cases for all of the arithmetic operators are straightforward, that is, the substitution is simply applied to the operands inductively. The Boolean substitution function is defined analogously, using the integer substitution function where required (for example, in the comparison operators).
96+
97+
[^1] One might think, given the base cases of the substitutions in which integers and Booleans evaluate to themselves, that these side conditions are not necessary. However, if they were removed, `K` would simply keep attempting to rewrite the final obtained value using the substitution, and this would keep succeeding, the value would keep being rewritten to itself, and the evaluation wound not terminate.
98+
99+
## Compiling and running the exercise
100+
101+
Follow the instructions from the top-level [`README`](../README.md) file to compile this exercise and run the provided tests. Create some further examples and/or change the hard-coded variables and their values to check if you get back the expected results.

0 commit comments

Comments
 (0)