CS208 Coursework 2026-2027

This is the coursework for semester one of CS208 Logic and Algorithms 2026/27.

It is worth 10% towards your final mark for all of CS208 (both semesters). The remainder of the marks come from the quizzes (5%), the algorithms coursework(s) in semester two (15%), and a final exam in April/May 2026 (70%).

The whole page is marked out of 20.

The questions are on this page, along with places for you to write your answers. This page will remember the answers you type in, even if you leave the page and come back. Your browser's local storage API is used to store the data. If you delete saved data in your browser, or visit this page in private browsing mode and then close the window, you will lose your answers.

Once you have completed the questions, click on the “Download” button to download your answers as a file called cs208-2026-coursework.answers. When you are ready to submit your answers, upload the file to the MyPlace submission page.

The deadline is 12:00 Wednesday 2nd December. All extension requests should be submitted via MyPlace.

Q0 (0 marks)

Enter your name and registration number:

• Name:

  <name>

• Registration number:

  <registration-number>

Q1 : Undefined Behaviour (2 marks)

The document defining the C programming language (available for free as a draft copy) includes the concept of undefined behaviour (Section 3.5.3). This means that there are things that have the syntax of C programs but the C standard does not assign them a behaviour for all possible inputs. A standards conforming C compiler is allowed to assume that the program it is asked to compile will only ever use behaviour that is defined by the standard. Therefore, if the program does do something that is undefined, then the C compiler is under no obligation to do anything “sensible” with the program.

The concept of undefined behaviour is surprisingly subtle. Usually we can rely on each part of a program having a well defined meaning. Sequential steps of a program apply those meanings one after the other until the program finishes. However, if the compiler is allowed to assume that some things cannot happen because doing so would lead to undefined behaviour then the compiler can draw surprising and non-obvious conclusions about the code.

Have a look at this snippet of C code. Assume that the variable ptr has type int * (i.e., it has the type of a pointer to an int).

if (ptr == NULL) {
  printf("ptr is NULL\n");
}
*ptr = 17;

We might hope to read this as “if ptr is NULL then print a message. Then write 17 into the memory location pointed to by ptr”. If ptr is actually NULL when this code gets executed then we might expect it to crash with a segmentation fault on the last line. But we would also expect it to have printed a message before that, helping us to diagnose the problem.

Surprisingly, the C standard does not require the compiler to print the message. In fact, the compiler is free to completely remove the whole if ... { ... } from the code.

The reason is that writing to a NULL pointer is undefined behaviour according to the C standard (Section 6.5.4.2, see footnote 101). Because a compiler is allowed to assume that the program will never use undefined behaviour, it is allowed to assume that ptr is not NULL. Therefore, the condition ptr == NULL cannot possibly be true, and therefore the body of the if will never run.

The chains of reasoning get quite long, so let's see how to model this situation using logic. We will use the following vocabulary to talk about an abstracted form of C programs:

1. NULL() will be the constant NULL value.

2. dereferenced(x) will be true if the variable x is dereferenced (i.e., read from or written to) at any point in the program.

3. message-printed is true if the message is printed.

On this vocabulary, we have several axioms. The first defines the rule above from the C standard: if a pointer is used, then it cannot be NULL:

We also encode the program into three axioms, which describe the programs' behaviour:

1. If ptr is NULL then the message gets printed:

   ptr = NULL() → message-printed

2. If ptr is not NULL then the message does not get printed (this is implicit in the empty else branch in the program):

   ¬ptr = NULL() → ¬message-printed

3. The variable ptr gets dereferenced (for this example, it does not matter what actual value gets written to *ptr):

With all of these axioms together, we can prove that the message does not get printed. Prove this using the proof tool:

This proof does not make any prior assumptions on what ptr is, so we can conclude that the message never gets printed even if ptr is NULL!

In fact, if ptr is NULL then the compiler has complete freedom to do whatever it wants, including making demons fly out of your nose. To model the possibility of nasal demonic transit we add the propositional atom nasal-demons to our vocabulary.

Now prove that the axioms above plus the fact that ptr = NULL() allows the compiler to justify nasal-demons:

What makes C's undefined behaviour so confusing from a programmer's point of view is that the consequences of invoking undefined behaviour (in this example, dereferencing a NULL pointer) can flow backwards through the program. Normally, we expect that a part of a program may fail or work in an unexpected way, but the consequences of this ought to happen after that. It is inherent in the way that C compilers optimise code that information about what will happen “in the future” of a program's execution flows backwards.

int unused = *ptr;
if (ptr == NULL) {
  printf("ptr is NULL\n");
}
*ptr = 17;

*ptr = 17;

Q2 : Set Theory (3 marks)

Predicate logic can be used as a foundational language for all of mathematics, but to do so we need to start from some axioms about what sort of things exist. Set Theory is a way of defining what mathematical things exist in terms of collections, called sets. The most common system of axioms for set theory is Zermelo-Fraenkel Set Theory which specifies 9 axioms (or "axiom schemas") that is enough to build almost all of modern mathematics. For this question we will look at two of the axioms: pairing and union.

In Set Theory, the only things that exist are sets and the only relationship that we have between things is membership. Membership is usually written as x ∈ y to mean x is a member of y (or x is an element of y). Here we will write this as member(x,y). Everything in Set Theory is built from sets and the membership relation between them.

Informally, we write sets by listing their elements inside curly brackets. For example, { a, b, c } is the set containing a, b and c. To express this in terms of the member relation we say that there exists a set x such that member(a,x), member(b,x) and member(c,x), and that for all y such that member(y,x) then y = a or y = b or y = c. Note that we have to give both a list of things that we know to be in the set and something that is true for everything in the set. (Compare to the introduction and elimination rules for the logical connectives.)

Saying that something is in a set twice (e.g., member(a,x) /\ member(a,x)) is equivalent to saying it is in the set once member(a,x). This matches the usual idea of sets that duplicates don't matter: the set { a, a } is the same as the set { a }.

There are nine axioms in the usual description of ZF Set Theory. Most of the axioms tell us when certain sets exist. We will only look at two of them:

1. The pair axiom says that if x and y are sets, then there exists a set p such that x and y are members of p, and that x and y are the only members of p.

   ∀x. ∀y. ∃p. (∀w. member(w, p) → (w = x ∨ w = y)) ∧ member(x, p) ∧ member(y, p)

   Informally, the pair axiom says that if we have x and y, then the set { x, y } exists.

2. The union axiom says that it is possible to “flatten” nested sets. For example, if we have a set of sets

     { {a, b, c}, {d, e, f}, {g, h}, {i} }
   

   then the union of these is all their elements flattened into one:

     { a, b, c, d, e, f, g, h, i }
   

   In general, if x is a set, then there exists a set z such that (1) for every w and u such that w ∈ u and u ∈ x then w ∈ z; and (2) if w ∈ z then there exists a u such that u ∈ x and w ∈ u.

   Expressed in logic, we write this as:

   ∀x. ∃z. (∀w. ∀u. member(w, u) → member(u, x) → member(w, z)) ∧ (∀w. member(w, z) → (∃u. member(u, x) ∧ member(w, u)))

Q2(a) : Making Singletons

Prove that the pairing axiom implies that singleton sets exist. That is, for every x, there is a set s that contains x and only x. This set is usually written as {x}.

Q2(b) : Unions of two sets

The union axiom states that a set of sets can be “flattened” to a single set by combining all their elements. A useful special case of this is the union of two sets: if x and y are sets, then their union (usually written x ∪ y) contains all the elements of x and all the elements of y and nothing else.

Prove that the union of x and y exists as a consequence of the pairing and union axioms:

Q2(c) : Making triples

The pairing axiom says that we can form the set {x,y} from x and y. Part (a) above says we can form {x} from x. Prove that from x, y, z we can make the set {x,y,z}.

Q3 : Hoare Logic is Sound (3 marks)

We have described the rules of Hoare Logic, but have not proved them sound with respect to our simple model of computation. You will do this now.

The rules are given here in a slighly more standard way than the way that the tool presents them. The tool presents a "forward first" approach that traces the path of a formula throughout the program starting at the start, while the standard approach is unbiased and allows the proof to explore the program in any order.

We will be using the definition of a Hoare Logic triple {P} prog {Q} in terms of the exec predicate:

In words: if P is true for the initial state s1, and executing prog get us from state s1 to state s2, then Q is true of the final state s2.

For the rules below (except for Consequence), we will have to assume certain properties of the exec predicate for the relevant kinds of program. We introduce these as we go.

Q3(a) : Logical Consequence

The Consequence rule allows a specification to be adjusted. If we know that prog satisifies the specification { P } prog { Q }, then we can strengthen the precondition and weaken the postcondition. Strengthening means assuming something that implies P, i.e. assuming something “stronger” (in the sense it can imply more things) than P. Weakening means ensuring something that is implied by Q.

As a deduction rule, Consequence is:

Prove that Hoare Triples satisfy Consequence:

Q3(b) : Doing Nothing

The simplest program is one that does nothing. In the tool this is called end because it is only ever needed at the end of a block of code. In the unbiased presentation of Hoare Logic it can be used anywhere and so is called skip() (it is similar to pass in Python).

To be able to state and prove a Hoare Logic rule for skip(), we need to write down in Logic how it works. The following formula describes the effect that skip() has on the state. It does nothing: the final state after doing skip() is the same as the state before.

The unbiased deduction rule for skip() is:

Similarly to the way that skip() does nothing to states, the rule says that anything that is true before skip() is true afterwards.

Prove that this rule is sound from the axiom about how skip() affects the state:

Q3(c) : Sequencing

The next basic way programs work is by sequencing them one after the other. The tool handles this implicitly, but the unbiased presentation of Hoare Logic treats sequencing as its own rule.

In the logic, we write the sequencing of two programs as seq(p1,p2). The behaviour of this program is specified by this formula:

In words: if execution of the sequence p1;p2 goes from state s1 to state s2, then there is an intermediate state s such that p1 goes from s1 to s and p2 goes from s to s2.

As with skip(), the Hoare Logic rule for sequencing follows the same shape. If there is an intermediate predicate R, then we can prove Hoare Triple for the sequencing of two programs.

Prove that this rule is sound from the axiom of how sequencing affects the state:

Q3(d) : Assignment (backward)

In the tool, updating the state is performed by writing to variables. In the simple model of programs we have here, the state is not necessarily made of separate variables. We will simply model the updating of the state by assuming that there is some function doUpdate(s) that returns the updated version of the state.

With this, we can specify the behaviour of the program update() which, when it executes starting in state s1, ensures that the final state is doUpdate(s1).

In the unbiased version of Hoare Logic, there are two possibilities for the deductive rule for update(). The first is the “backwards” rule:

This rule states that if P was true assuming we already did the update, then P is true afterwards. This version of the rule is useful for reasoning backwards through the program to produce a weakest precondition.

Prove that this rule is sound, assuming the update axiom for exec:

Q3(e) : Assignment (forward)

The alternative version of the rule for update() reasons forwards. This is the form that is used in the tool. The rule is:

This rule is perhaps easier to explain. If P is true about the current state before the update, then after the update there exists an old state, where the new states is equal to the update of the old state and P is true about the old state.

Prove this rule using the same axiom for update() as above:

Q3(f) : If-then-else

If-then-else is more complex than the rules above because it involves branching between two possible outcomes, so there are two premises to the rule.

Formalising the behaviour of if-then-else on an arbitrary boolean expression will be too complicated, so here we just assume there is some condition C on states that is being tested.

The axiom describing the behaviour of a successful execution of an if-then-else on condition C is:

In words: if ifC(p1,p2) executes from state s1 to state s2, then either C(s1) was true and p1 did that execution, or C(s1) was not true and p2 did that execution.

The rule for ifC follows this idea. The OR in the formula becomes a requirement to prove two premises, because we do not know which of them will be true:

Use the exec-if axiom to prove that the If rule is sound in Hoare Logic:

Q4 : Straight Line Programs (3 marks)

These three sub-questions all involve proving something about programs that do not involve any loops using the rules of Hoare Logic. You will also find assertions and automation useful.

Q4(a) : One step forward, one step back

Adding and then subtracting gets you back to where you started:

Use this fact to write the following program that ends with a copy of X in Y and the sum of them in X. You should be able to write the program with one assignment to each of X and Y.

HINT: The final proof will involve spliting, rewriting the goal using add-sub, and then auto. It might be easier to see what is going on if you put an assert just before the final line of the program that describes the final values of X and Y in terms of x and y (and add and sub) without any indirections through oldX and oldY.

Q4(b) : Swapping with XOR

The bitwise xor function on pairs of integers has the following two useful properties:

1. It is commutative:

   ∀x. ∀y. xor(x, y) = xor(y, x)

2. It is cancellative, meaning that xoring with the same value twice gets you back to where you started.

   ∀x. ∀y. xor(xor(x, y), y) = x

These two properties mean that it is possible to write a swapping program on integers that does not use a temporary variable.

X := xor(X,Y)
Y := xor(X,Y)
X := xor(X,Y)

Prove that this program works. The program code you type in (excepting assert statements) should be exactly the three lines above.

HINT: The proof will be much easier if you put an assert after each line of code rewriting the formula for the state at that point as a pair of equations /\d together, one for X and one for Y.

Q4(c) : Swapping Array Elements

This program swaps two elements of an array A at indexes I and J. All other elements of the array are left as they were before:

Temp := get(A,I)
A := set(A, I, get(A, J))
A := set(A, J, Temp)

Using the axioms for arrays, write a proof that this program satisfies the specification. We assume that I and J are different to cut down on cases in the proof, although the program does still work in this case.

You can add as many asserts as you need, but the program code should be exactly the same as above.

HINT: It is useful to add an assert at the end of the program but before end that summarises in one line how the final value of A relates to the initial value of the array in arr.

Q5 : Programs with Loops (3 marks)

The next three questions involve programs with loops. The programs are given to you, but to complete the proofs you will need to work out the right loop invariant to use, and how to use the axioms given to complete the proof.

Q5(a) : Counting

The following program counts up the number of times lookup(I) returns 0 between 0 and LEN - 1:

I := 0
COUNT := 0
while (I != LEN) {
  if (lookup(I) = 0) {
    COUNT := add(COUNT,1)
  }
  I := add(I,1)
}

We will specify this program using a function called countTo which is defined by the following axioms:

1. There are zero items up to index 0, so the count is 0:

   countTo(0) = 0

2. If lookup(i) = 0 then counting up to i + 1 is one more than counting up to i:

   ∀i. lookup(i) = 0 → countTo(add(i, 1)) = add(countTo(i), 1)

3. If ¬lookup(i) = 0 then counting up to i + 1 is the same as counting up to i:

   ∀i. ¬lookup(i) = 0 → countTo(add(i, 1)) = countTo(i)

Prove that the program above correctly implements countTo. You can add as many asserts as you need, but the program code should be exactly the same as above.

Q5(b) : Summing

The following program sums up the numbers in an array A up to but not including the Nth element., putting the result into the variable SUM.

I := 0
SUM := 0
while (I != N) {
  SUM := add(SUM,get(A,I))
  I := add(I,1)
}

The behaviour of this program can be specified by the following pair of equations:

1. Summing up to the 0th element is 0:

   ∀arr. sumArray(arr, 0) = 0

2. Summing up to the n+1th element is summing up to the nth element plus the nth element:

   ∀arr. ∀i. sumArray(arr, add(i, 1)) = add(sumArray(arr, i), get(arr, i))

Prove that the program above correctly implements sumArray. You can add as many asserts as you need, but the program code should be exactly the same as above.

Q5(c) : Running Sum

The following program computes the running sums of an array A. At the end of the program, the output array B at element i contains the sum of the elements of A up to i.

SUM := 0
I := 0
while (I != N) {
  B := set(B, I, SUM)
  SUM := add(SUM, get(A, I))
  I := add(I,1)
}

Prove that this program satisfies the specification written above. You will need to use the sumArray axioms from before with the array get and set axioms and the axioms for between from the page on Hoare logic with arrays.

You can add as many asserts as you need, but the program code should be exactly the same as above.

Q6 : Register Allocation (3 marks)

Compilers have to translate from high level code that uses any amount of variables to low-level machine code that only has as many registers as the CPU has. Each variable in the high-level code must be assigned to a register in the machine code, but since there may be fewer registers than variables in the original code we have to find a way of reusing registers where possible. This is a kind of resource allocation problem. One way to solve this problem is to express the problem in terms of logical constraints and ask the computer to find a solution. We will do this by expressing valid allocations as models of logical theories.

As an example, we will look at the following program (though the solution you will write should work for any program by changing the constraints). The program uses six variables, and is written in Static Single Assignment (SSA) form. This means that every variable is only written to once, which makes things easier (most modern compilers use SSA internally).

1. X = 5
2. Y = 6
3. Z = X + Y
4. W = X + Z
5. U = W + Z
6. V = U + X
7. return V

Let's say we are compiling to a machine with only three registers R1, R2, R3. To systematically work out how to assign registers to variables, we need to work out the "live ranges" of each variable: the range of instructions for which a variable is required to have a place to call its own. If two variables have overlapping live ranges then they must be stored in separate registers. If not they can "share" a register.

For this program, the live ranges for each variable are as follows, where the starting instruction is when it gets assigned and the finish instruction is the last time it is used.

X : 1 to 6
Y : 2 to 3
Z : 3 to 5
W : 4 to 5
U : 5 to 6
V : 6 to 7

If two variables have ranges (s1,e1) and (s2,e2), then they can only share a register if either e1 <= s2 or e2 <= s1 (it is ok for the start of one to be the same as the end of another if we assume that the add instruction can write to the same register as one of its arguments). If two variables have overlapping live ranges then they conflict.

Question

1. Complete the theory RegisterAllocation below by filling in the axiom definitions to make sure that for any model of this theory, allocated is a valid allocation of variables to registers avoiding conflicts.

2. Fill in the empty definitions in the model Example to accurately model the register allocation problem described above. The universe has been filled in for you.

Q7 : Planning (3 marks)

A planning problem is where we are asked to invent a way of achieving a goal by making actions. We can use logic to solve many kinds of planning problem. Given a logical description of what it means to be a good plan and constraints on what actions can be taken, we can get computers to write plans for us. In this question you will develop a simple logical description of good plans that can be used by the computer to generate plans to meet specific goals.

You are asked to write a theory for describing plans where a robot has to be in a sequence of locations, one for each timestep. Across consecutive timesteps, the robot can only move between locations that are linked. The robot must hit several specified waypoints.

To define what we mean by a plan, we need to represent times and places logically.

Time

We model time as a collection of timesteps related to each other by a relation next/2. The idea is that timesteps are any t for which timestep(t) is true, and two timesteps are consecutive if the relation next(t1,t2) is true.

We will not specify any particular axioms about time in our theory. The nature of time will be something that is given by the model itself. For some purposes, it might make sense for time to be have branches or to have loops.

For the example planning scenario here though, we will assume that there are six timesteps T1, T2, T3, T4, T5, T6, and that next(x,y) is true for each pair in sequence. Only immediately consecutive timesteps are related by next: we have next(T1,T2) and next(T2,T3) but not next(T1,T3).

Place

We model the places that can be moved to as locations related to each other by linked/2. Locations are things l such that location(l) is true. Two locations l1 and l2 are directly linked if linked(l1,l2) is true. The idea is that if two locations are linked, then the robot can move from one to the other in between two immediately subsequent timesteps.

For the example planning scenario here, we assume the locations Store, Factory, LoadingBay, Road, Yard, and WasteHeap. These are linked in the following way:

    (Store, Factory)
    (Store, Yard)
    (Factory, Store)
    (Factory, LoadingBay)
    (Yard, Factory)
    (Yard, Store)
    (Yard, WasteHeap)
    (WasteHeap, Road)
    (WasteHeap, Yard)
    (LoadingBay, WasteHeap)
    (LoadingBay, Factory)
    (LoadingBay, Road)

Waypoints

A waypoint is a particular (time,location) pair that must be met during the plan. We represent these using a predicate waypoint/2.

In the example here, we want the robot to be in the Store at timestep T1 and at the Road at timestep T6.

Representing Plans

We represent a plan using a predicate robot-at/2. If we have robot-at(t,l), then at timestep t the robot is at location l. To be a valid plan, this predicate must satisfy the following properties:

1. If the robot at time t is at l, then t is a timestep and l is a location.

2. At every timestep, the robot is at some location.

3. The robot is never in more than one location at each timestep.

4. For each consecutive pair of timesteps t1 and t2, the location at time t1 and the location at time t2 are linked.

5. Each waypoint is met by the robot.

Plans are Models

The editor box below is set up with a theory with the vocabulary described above and a partial model of this vocabulary for the example planning problem.

If you click ‘Run’, it will generate an empty plan (i.e., an empty definition of robot-at/2 where nothing is true). The empty plan is not a valid plan.

Add axioms to the theory that generate a valid plan for the robot. Make sure that your axioms match the five properties for a good plan listed above. You should put in the axioms that match the properties above, not just ones that happen to give a valid plan in this example. Your axioms should work for all examples.

Remember to download your answers and submit them to MyPlace.