COMP3610/6361 Principles of Programming Languages
Principles of Programming Languages
Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
COMP3610/6361 Principles of Programming Languages
Assignment 1
ver 1.0
Submission Guidelines
• Due time: Aug 10, 2023, 11am (Canberra Time) Aug 13, 2023, 11:59pm (Canberra Time)
• Submit a pdf via Wattle.
• Scans of hand-written text are fine, as long as they are readable and neat.
• Please read and sign the declaration on the last page and attach a copy to your submission.
• No late submission, deadline is strict
Exercise 1 (Syntax) (30 Marks)
Type checking can be done with help of a type system, or with a refined syntax – to a certain degree.
Question 1 Refine the syntax given on Slide 33 of Lecture 1 (IMP – Syntax), such that it can distinguish
boolean expressions, integer expressions and program expressions.
Question 2 Explain in a few sentences your design decisions: you can, for example, explain which
expressions are excluded and which are not (and why this makes sense). To get you started, you may ask
yourself whether the expression
while 5≥ (if !l ≥ 3 then 3 else 6) do l := !l+1
should be allowed. Parentheses are only given to help the reader.
Exercise 2 (Semantics) (25 Marks)
We extend the syntax of our simple while language to be the following:
Booleans b ∈ B = {true,false}
Integers (Values) n ∈ Z = {. . . ,−1,0,1, . . .}
Locations l ∈ L = {l, l0, l1, l2, . . .}
Operations op::=+ | ≥ | ∧
Expressions
E ::= n | b | E op E |
l := E | !l |
if E then E else E |
skip | E ; E |
while E do E |
Question 3 The operator ∧ denotes Boolean conjunction. Extend the sos-rules (operational semantics)
to define the ‘standard’ behaviour of ∧.
2 COMP3610/6361
Question 4 Extend the syntax and the semantics with a (nondeterministic) choice operator ⊔. The idea
is that E1⊔E2 can freely choose between E1 and E2 as long as Ei (1≤ i≤ 2) is not stuck.
Exercise 3 (Types) (10 Marks)
Give a derivation tree to prove that
{} ⊢ if 3≥ 7 then 3+5 else 4: int
is well typed.
Exercise 4 (A Well-typed Program) (35 Marks)
Question 5 Write a program P in the simple imperative language of the lecture that computes the
factorial of the integer initially stored in location l1. Make sure that you only use the syntax given on
Slide 33 of the first lecture.
Question 6 Prove that your program P is well typed. That means, give a type derivation for
l1 : intref ⊢ P :unit
P. Ho¨fner 3
Academic Integrity
I declare that this work upholds the principles of academic integrity, as defined in the University Aca-
demic Misconduct Rule; is entirely my own work, with only the exceptions listed; is produced for the
purposes of this assessment task and has not been submitted for assessment in any other context, except
where authorised in writing by the course convener; gives appropriate acknowledgement of the ideas,
scholarship and intellectual property of others insofar as these have been used; in no part involves copy-
ing, cheating, collusion, fabrication, plagiarism or recycling.