CS320 Fall2023 Project Part 1
November 2023
1 Overview
Stack-oriented programming languages utilize one or more stack data structures which the programmer manipulates
to perform computations. The specification below lays out the syntax and semantics of such a language
which you will need to implement an evaluator for, taking a program and evaluating it into an OCaml value.
You must implement a function:
interp : string -> string list option
Where the input string is some (possibly ill-formed) stack-language program and the result is a list of things
“printed” by the program during its evaluation.
1
2 Grammar
For part 1, you will need to support the following grammar. The grammar specifies the form of a valid program.
Any invalid program, one which is not derivable from the grammar, cannot be given meaning and evaluted. In
the case of an invalid program, interp should return None. ⟨prog⟩ is the starting symbol.
2.1 Constants
⟨digit⟩ ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
⟨nat⟩ ::= ⟨digit⟩ | ⟨digit⟩⟨nat⟩
⟨int⟩ ::= ⟨nat⟩ | -⟨nat⟩
⟨bool⟩ ::= True | False
⟨const⟩ ::= ⟨int⟩ | ⟨bool⟩ | Unit
2.2 Programs
⟨prog⟩ ::= ⟨coms⟩
⟨com⟩ ::= Push ⟨const⟩ | Pop | Trace
| Add | Sub | Mul | Div
| And | Or | Not
| Lt | Gt
⟨coms⟩ ::= ϵ | ⟨com⟩; ⟨coms⟩
Note: ϵ is the empty symbol. We use ϵ to refer to empty strings or empty lists depending on context.
2
3 Operational Semantics
For part 1, you will need to support the following operational semantics. The operational semantics specifies
the meaning of a valid program. For the stack-language, a program is evaluated using a stack and it produces
a trace. Once we have fully evaluated the program, we return the resulting trace from interp.
3.1 Configuration of Programs
A program configuration is of the following form.
[ S | T ] P
• S: (Stack) stack of intermediate values
• T: (Trace) list of strings logging the program trace
• P: (Program) program commands to be interpreted
Examples:
[ ϵ | ϵ ] Push True; Not; Push 1; Lt; ϵ (1)
[ 1 :: 2 :: ϵ | "True" :: "0" :: ϵ ] Push True; Push 9; Pop; ϵ (2)
[ 0 :: True :: ϵ | ϵ ] Push 10; Push 9; Add; Trace; ϵ (3)
[ True :: False :: 321 :: ϵ | "123" :: "False" :: ϵ ] Pop; Pop; Trace; Gt; ϵ (4)
3.2 Program Reduction
The operational semantics of the language is defined in terms of the following single step relation.
[ S1 | T1 ] P1 ⇝ [ S2 | T2 ] P2
In one step, program configuration [ S1 | T1 ] P1 evaluates to [ S2 | T2 ] P2. For configurations where P = ϵ, we
say that evaluation has terminated as there is no program left to interpret. In this case, return trace T as the
final result of your interp function.
3.3 Push
Given any constant c, the command Push c pushes c onto the current stack S. Push never fails.
Push
[ S | T ] Push c; P ⇝ [ c :: S | T ] P
Examples:
• [ 1 :: True :: ϵ | "Unit" :: "False" :: ϵ ] Push 2; ϵ ⇝ [ 2 :: 1 :: True :: ϵ | "Unit" :: "False" :: ϵ ] ϵ
• [ 1 :: True :: ϵ | "5" :: ϵ ] Push True; ϵ ⇝ [ True :: 1 :: True :: ϵ | "5" :: ϵ ] ϵ
3
3.4 Pop
Given a stack of the form c :: S (constant c is on top of S), the Pop command removes c and leaves the rest of
stack S unmodified.
The Pop command has 1 fail state.
1. PopError: The stack is empty (S = ϵ).
When Pop fails, the string "Panic" is prepended to the trace and the program terminates.
PopStack
[ c :: S | T ] Pop; P ⇝ [ S | T ] P
PopError
[ ϵ | T ] Pop; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 1 :: True :: ϵ | "Unit" :: "False" :: ϵ ] Pop; ϵ ⇝ [ True :: ϵ | "Unit" :: "False" :: ϵ ] ϵ
• [ ϵ | "5" :: ϵ ] Pop; Push 12; ϵ ⇝ [ ϵ | "Panic" :: "5" :: ϵ ] ϵ
3.5 Trace
Given a stack of the form c :: S where c is any valid constant, the Trace command removes c from the stack
and puts a Unit constant onto the stack. The string representation of c as determined by the toString function
to prepended to the trace.
The Trace command has 1 fail state.
1. TraceError: The stack is empty (S = ϵ).
When Trace fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
TraceStack
[ c :: S | T ] Trace; P ⇝ [ Unit :: S | toString(c) :: T ] P
TraceError
[ ϵ | T ] Trace; P ⇝ [ ϵ | "Panic" :: T ] ϵ
The toString function is a special function which you must define to convert constant values into their string
representations. The following equations illustrate the strings expected for typical inputs.
toString(123) = "123" (1)
toString(True) = "True" (2)
toString(False) = "False" (3)
toString(Unit) = "Unit" (4)
Examples:
• [ 1 :: True :: ϵ | "Unit" :: "False" :: ϵ ] Trace; ϵ ⇝ [ Unit :: True :: ϵ | "1" :: "Unit" :: "False" :: ϵ ] ϵ
• [ ϵ | "5" :: ϵ ] Trace; Push 12; ϵ ⇝ [ ϵ | "Panic" :: "5" :: ϵ ] ϵ
4
3.6 Add
Given a stack of the form i :: j :: S where both i and j are integer values, the Add command removes i and j
from the stack and puts their sum (i + j) onto the stack.
The Add command has 3 fail states.
1. AddError1: Either i or j is not an integer.
2. AddError2: The stack is empty (S = ϵ).
3. AddError3: The stack has only 1 element (S = c :: ϵ).
When Add fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
AddStack
i and j are both integers
[ i :: j :: S | T ] Add; P ⇝ [ (i + j) :: S | T ] P
AddError1
i or j is not an integer
[ i :: j :: S | T ] Add; P ⇝ [ ϵ | "Panic" :: T ] ϵ
AddError2
[ ϵ | T ] Add; P ⇝ [ ϵ | "Panic" :: T ] ϵ
AddError3
[ c :: ϵ | T ] Add; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Add; ϵ ⇝ [ 9 :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: True :: Unit :: ϵ | "False" :: ϵ ] Add; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ 4 :: ϵ | "False" :: ϵ ] Add; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
3.7 Sub
Given a stack of the form i :: j :: S where both i and j are integer values, the Sub command removes i and j
from the stack and puts their difference (i − j) onto the stack.
The Sub command has 3 fail states.
1. SubError1: Either i or j is not an integer.
2. SubError2: The stack is empty (S = ϵ).
3. SubError3: The stack has only 1 element (S = c :: ϵ).
When Sub fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
SubStack
i and j are both integers
[ i :: j :: S | T ] Sub; P ⇝ [ (i − j) :: S | T ] P
SubError1
i or j is not an integer
[ i :: j :: S | T ] Sub; P ⇝ [ ϵ | "Panic" :: T ] ϵ
SubError2
[ ϵ | T ] Sub; P ⇝ [ ϵ | "Panic" :: T ] ϵ
SubError3
[ c :: ϵ | T ] Sub; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Sub; ϵ ⇝ [−1 :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: True :: Unit :: ϵ | "False" :: ϵ ] Sub; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ 4 :: ϵ | "False" :: ϵ ] Sub; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
5
3.8 Mul
Given a stack of the form i :: j :: S where both i and j are integer values, the Mul command removes i and j
from the stack and puts their product (i °ø j) onto the stack.
The Mul command has 3 fail states.
• MulError1: Either i or j is not an integer.
• MulError2: The stack is empty (S = ϵ).
• MulError3: The stack has only 1 element (S = c :: ϵ).
When Mul fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
MulStack
i and j are both integers
[ i :: j :: S | T ] Mul; P ⇝ [ (i °ø j) :: S | T ] P
MulError1
i or j is not an integer
[ i :: j :: S | T ] Mul; P ⇝ [ ϵ | "Panic" :: T ] ϵ
MulError2
[ ϵ | T ] Mul; P ⇝ [ ϵ | "Panic" :: T ] ϵ
MulError3
[ c :: ϵ | T ] Mul; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Mul; ϵ ⇝ [ 20 :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: True :: Unit :: ϵ | "False" :: ϵ ] Mul; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ 4 :: ϵ | "False" :: ϵ ] Mul; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
6
3.9 Div
Given a stack of the form i :: j :: S where both i and j are integer values, the Div command removes i and j
from the stack and puts their quotient (i °¿ j) onto the stack.
The Div command has 4 fail states.
1. DivError0: Both i and j are integers and j = 0.
2. DivError1: Either i or j is not an integer.
3. DivError2: The stack is empty (S = ϵ).
4. DivError3: The stack has only 1 element (S = c :: ϵ).
When Div fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
DivStack
i and j are both integers, j ̸= 0
[ i :: j :: S | T ] Div; P ⇝ [ (i °¿ j) :: S | T ] P
DivError0
i is an integer
[ i :: 0 :: S | T ] Div; P ⇝ [ ϵ | "Panic" :: T ] ϵ
DivError1
i or j is not an integer
[ i :: j :: S | T ] Div; P ⇝ [ ϵ | "Panic" :: T ] ϵ
DivError2
[ ϵ | T ] Div; P ⇝ [ ϵ | "Panic" :: T ] ϵ
DivError3
[ c :: ϵ | T ] Div; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 16 :: 8 :: True :: Unit :: ϵ | "False" :: ϵ ] Div; ϵ ⇝ [ 2 :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 16 :: 0 :: True :: Unit :: ϵ | "False" :: ϵ ] Div; Push Unit; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ 16 :: True :: Unit :: ϵ | "False" :: ϵ ] Div; Add; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ 4 :: ϵ | "False" :: ϵ ] Div; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
7
3.10 And
Given a stack of the form a :: b :: S where both a and b are boolean values, the And command removes a and b
from the stack and puts their conjunction (a ∧ b) onto the stack.
The And command has 3 fail states.
1. AndError1: Either a or b is not a boolean.
2. AndError2: The stack is empty (S = ϵ).
3. AndError3: The stack has only 1 element (S = c :: ϵ).
When And fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
AndStack
a and b are both booleans
[ a :: b :: S | T ] And; P ⇝ [ (a ∧ b) :: S | T ] P
AndError1
a or b is not a boolean
[ a :: b :: S | T ] And; P ⇝ [ ϵ | "Panic" :: T ] ϵ
AndError2
[ ϵ | T ] And; P ⇝ [ ϵ | "Panic" :: T ] ϵ
AndError3
[ c :: ϵ | T ] And; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ True :: True :: Unit :: ϵ | "False" :: ϵ ] And; ϵ ⇝ [ True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ False :: True :: Unit :: ϵ | "False" :: ϵ ] And; Trace; ϵ ⇝ [ False :: Unit :: ϵ | "False" :: ϵ ] Trace; ϵ
• [ True :: 4 :: Unit :: ϵ | "False" :: ϵ ] And; Pop; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
3.11 Or
Given a stack of the form a :: b :: S where both a and b are boolean values, the Or command removes a and b
from the stack and puts their disjunction (a ∨ b) onto the stack.
The Or command has 3 fail states.
1. OrError1: Either a or b is not a boolean.
2. OrError2: The stack is empty (S = ϵ).
3. OrError3: The stack has only 1 element (S = c :: ϵ).
When Or fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
OrStack
a and b are both booleans
[ a :: b :: S | T ] Or; P ⇝ [ (a ∨ b) :: S | T ] P
OrError1
a or b is not a boolean
[ a :: b :: S | T ] Or; P ⇝ [ ϵ | "Panic" :: T ] ϵ
OrError2
[ ϵ | T ] Or; P ⇝ [ ϵ | "Panic" :: T ] ϵ
OrError3
[ c :: ϵ | T ] Or; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ True :: True :: Unit :: ϵ | "False" :: ϵ ] Or; ϵ ⇝ [ True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ False :: True :: Unit :: ϵ | "False" :: ϵ ] Or; Trace; ϵ ⇝ [ True :: Unit :: ϵ | "False" :: ϵ ] Trace; ϵ
• [ True :: 4 :: Unit :: ϵ | "False" :: ϵ ] Or; Pop; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
8
3.12 Not
Given a stack of the form a :: S where a is a boolean values, the Not command removes a from the stack and
puts its negation (°˛a) onto the stack.
The Not command has 2 fail states.
1. NotError1: a is not a boolean.
2. NotError2: The stack is empty (S = ϵ).
When Not fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
NotStack
a is a boolean
[ a :: S | T ] Not; P ⇝ [ (°˛a) :: S | T ] P
NotError1
a is not a boolean
[ a :: S | T ] Not; P ⇝ [ ϵ | "Panic" :: T ] ϵ
NotError2
[ ϵ | T ] Not; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ True :: Unit :: ϵ | "False" :: ϵ ] Not; ϵ ⇝ [ False :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: Unit :: ϵ | "False" :: ϵ ] Not; Pop; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
• [ ϵ | "False" :: ϵ ] Not; Add; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
3.13 Lt
Given a stack of the form i :: j :: S where both i and j are integer values, the Lt command removes i and j
from the stack and puts the boolean result of their comparison (i < j) onto the stack.
The Lt command has 3 fail states.
1. LtError1: Either i or j is not an integer.
2. LtError2: The stack is empty (S = ϵ).
3. LtError3: The stack has only 1 element (S = c :: ϵ).
When Lt fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
LtStack
i and j are both integers
[ i :: j :: S | T ] Lt; P ⇝ [ (i < j) :: S | T ] P
LtError1
i or j is not an integer
[ i :: j :: S | T ] Lt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
LtError2
[ ϵ | T ] Lt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
LtError3
[ c :: ϵ | T ] Lt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Lt; ϵ ⇝ [ True :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 5 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Lt; ϵ ⇝ [ False :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: True :: Unit :: ϵ | "False" :: ϵ ] Lt; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
9
3.14 Gt
Given a stack of the form i :: j :: S where both i and j are integer values, the Gt command removes i and j
from the stack and puts the boolean result of their comparison (i > j) onto the stack.
The Gt command has 3 fail states.
1. GtError1: Either i or j is not an integer.
2. GtError2: The stack is empty (S = ϵ).
3. GtError3: The stack has only 1 element (S = c :: ϵ).
When Gt fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
GtStack
i and j are both integers
[ i :: j :: S | T ] Gt; P ⇝ [ (i > j) :: S | T ] P
GtError1
i or j is not an integer
[ i :: j :: S | T ] Gt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
GtError2
[ ϵ | T ] Gt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
GtError3
[ c :: ϵ | T ] Gt; P ⇝ [ ϵ | "Panic" :: T ] ϵ
Examples:
• [ 4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Gt; ϵ ⇝ [ False :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 10 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Gt; ϵ ⇝ [ True :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 5 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ ] Gt; ϵ ⇝ [ False :: True :: Unit :: ϵ | "False" :: ϵ ] ϵ
• [ 4 :: True :: Unit :: ϵ | "False" :: ϵ ] Gt; Trace; ϵ ⇝ [ ϵ | "Panic" :: "False" :: ϵ ] ϵ
10
4 Full Examples
• Compute the polynomial x2 − 4x + 7 at 3:
Push 3;
Push 3;
Mul;
Push -4;
Push 3;
Mul;
Add;
Push 7;
Add;
Trace;
Result: Some ["4"]
• De Morgan’s Law:
Push False;
Push False;
And;
Not;
Trace;
Push False;
Not;
Push False;
Not;
Or;
Trace;
Result: Some ["True"; "True"]
• x2 is monotonic:
Push 2;
Push 2;
Mul;
Push 3;
Push 3;
Mul;
Gt;
Trace;
Result: Some ["True"]
11