High Integrity Systems Engineering
Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
SWEN90010: High Integrity Systems Engineering
Assignment
1 Introduction
The assignment is worth 20% of your total mark and is done in pairs (the same pairs as assign-
ments 1 and 2, unless you have been re-allocated to a new pair).
The aim of this assignment is to use the SPARK Ada toolset to implement and verify the
correctness and security of a small command-line Desktop Calculator utility.
That is, your pair will implement the functionality of the calculator program (as specified below)
in SPARK Ada, and use the SPARK Prover to prove that it is free of runtime errors and,
additionally, that it is also secure.
As usual, get started early and use your pair to maximum advantage.
Download, install and check you can run the GNAT tools (see Section 3.1) ASAP!
2 The Calculator
The program you have to implement is a command-line utility for performing numerical calcu-
lations. It takes input from the terminal (i.e. standard input, aka stdin).
Tokens in the grammar above are separated by one or more whitespace characters, namely space,
tab, and line-feed. Each is a string of non-whitespace characters. is a
4-digit string of non-whitespace characters that represents a non-negative number (i.e. a natural
number) in the range 0000 . . . 9999.
1
• The calculator can be in one of two states, either locked or unlocked.
• When the user starts the calculator, they supply (via a command-line argument) a 4-digit
string masterpin that represents a 4-digit PIN (i.e. a number in the range 0000 . . . 9999),
which is the master PIN needed to unlock the calculator. If no master PIN is supplied,
the calculator should exit immediately.
• The calculator begins in the locked state.
• For a string pin that represents a 4-digit PIN, the command “unlock pin” does nothing
when the calculator is in the unlocked state. Otherwise, it checks whether pin is equal to
the master PIN and, if so, changes the state of the calculator to unlocked. If pin is not
equal to the master PIN, then the state of the calculator is not changed.
• For a string newpin that represents a 4-digit PIN, the command “lock newpin” does nothing
when the calculator is in the locked state. Otherwise, it updates the master PIN to become
newpin and changes the state of the calculator to locked.
• For a string num representing a decimal integer, e.g. “5”, the command “push num” pushes
the value represented by num onto operand stack.
• The command “pop” pops the value from the top of the operand stack, discarding it.
• The commands “+”, “-”, “*” and “/” each pop the top two values from the operand stack
and compute the corresponding arithmetic operation on them (addition, subtraction, mul-
tiplication and division, respectively), and push the result onto the stack.
• For a string var, the command “load var ” loads the value stored in variable var and pushes
it onto the stack.
• For a string var, the command “store var ” pops the value from the top of the stack and
stores it into variable var, defining that variable if it is not already defined.
• The command “list” prints out all currently defined variables and their corresponding values.
• For a string var, the command “remove var ” makes variable var undefined (i.e. it will not
be printed by subsequent “list” commands).
2.2 Notes
• The calculator only takes input from the terminal (i.e. from stdin).
• When the calculator is started, the user supplies on the command line the master PIN, as
a command line argument.
• PINs are 4-digit strings in the range 0000 . . . 9999.
• The calculator can be in one of two states: either locked or unlocked.
• The “unlock” and “lock” commands change the state of the calculator between locked and
unlocked. The “lock” command allows updating the master PIN (see above).
• Variable names longer than 1024 characters are invalid.
2
• PINs that are not 4-digit strings in the range 0000 . . . 9999 are invalid.
• Input lines (i.e. commands) longer than 2048 characters are invalid.
• When receiving invalid input, the calculator should exit immediately (possibly after print-
ing an appropriate error message).
• When performing a calculation that would produce a result outside the range−231 . . . 231−1
inclusive (e.g. when computing −1×−231 the calculator is allowed to do whatever it wants
except it is not allowed to raise any Ada errors e.g. it cannot raise a CONSTRAINT_ERROR
etc. For instance it could choose not to perform the operation, or to exit immediately, etc.
• Similarly, when performing an operation that would cause division by zero, the calculator
should not raise an Ada error, but otherwise it is allowed to do whatever it wants e.g. do
nothing, exit immediately etc.
• Likewise, when performing an operation that would exceed the capacity of the operand
stack, the calculator is free to do whatever it wants except it cannot raise an Ada error.
Similarly for an operation for which there are insufficient operands on the stack.
• The capacity of the calculator’s operand stack is 512.
• Decimal integers in commands (e.g. “5” in “push 5”) that are outside the range −231 . . . 231−
1 inclusive are treated as representing 0.
2.3 A Demo Session with the Calculator
The user supplies the initial master PIN when starting the application, which is called main. For
example, to start the application setting the master PIN to “1234” the user would run:
$ ./main 1234
The calculator accepts commands from the user and its prompt indicates whether it is in the
locked or the unlocked state. Initially, it is always locked. Here is an example session showing
its expected output for valid commands.
$ ./main 1234
locked> unlock 1234
unlocked> push 5
unlocked> push 10
unlocked> *
unlocked> store a
unlocked> load a
unlocked> push 20
unlocked> *
unlocked> store b
unlocked> list
a => 50
b => 1000
unlocked> remove a
unlocked> list
3
b => 1000
unlocked> lock 2345
locked>
3 Your tasks
Get started early. This assignment is worth 20 marks in total.
3.1 Task -1: Download and Install GNAT Community Edition 2019
Download and install GNAT Community Edition from: https://www.adacore.com/download.
Ensure that the bin/ directory is in your PATH so that you can run the Ada tools directly. If
your setup is correct, you should be able to run commands like gnatmake and gnatprove and
see output like the following (noting that in this case the commands were run on MacOS):
$ gnatmake --version
GNATMAKE Community 2019 (20190517-83)
Copyright (C) 1995-2019, Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
$ gnatprove --version
2019 (20190517)
Why3 for gnatprove version 1.2.0+git
/Users/toby/opt/GNAT/2019/libexec/spark/bin/alt-ergo: Alt-Ergo version 2.3.0
/Users/toby/opt/GNAT/2019/libexec/spark/bin/cvc4: This is CVC4 version 1.7.1-prerelease
/Users/toby/opt/GNAT/2019/libexec/spark/bin/z3: Z3 version 4.8.0 - 64 bit
3.2 Task 0: Downloading and Building the Helper Code
You need to implement the calculator in SPARK Ada. However you are provided with some
helper code to get you started.
Download the ZIP file containing the helper code from the LMS. It contains a small number of
Ada packages:
• main.adb: a top level main program that shows basic usage of the other packages. You
will replace this with the top level of your calculator implementation.
• MyCommandLine: Provides a simple SPARK API for accessing command line arguments.
• MyString: Provides a simple SPARK abstract data type for strings. Used for representing
lines of input as well as variable names, command names, etc.
• MyStringTokeniser: Provides a simple SPARK interface for tokenising strings. By “to-
kenising” we mean to break a string up into its various whitespace-separated tokens (where
each token contains no whitespace).