[SOLVED] **HW 1: Due May 10, 2022, 23:59**

**HW 1: Due May 10, 2022, 23:59**

In this assignment, you will implement a verifier based on the weakest-precondition/VCGen methodology.

Copyright By Assignmentchef assignmentchef

We will work with programs that are written in a subset ECMAScript and translate them into our imperative language Nano.

Requirements

Install Microsofts Z3 SMT solver

Linux: https://www.howtoinstall.me/ubuntu/18-04/z3/
MacOs: https://formulae.brew.sh/formula/z3
Binaries: https://github.com/Z3Prover/z3/releases

Install Haskell/GHC and stack

Follow the installation instructions on https://docs.haskellstack.org/en/stable/README/

Make sure your machine has the above **requirements**.

After that, just clone the directory using

git clone https://github.com/gleissen/hw1.git

and youre good to go!

You can build and run the verifier with

$ stack run tests/pos/skip.js

Here, `tests/pos/skip.js` specifies the file we want to verify. If all went well
you should see something like:

hornConfig {files = [tests/pos/skip.js]}

Checking the file : tests/pos/skip.js
horn: TODO: FILL THIS IN!
CallStack (from HasCallStack):

After filling in the right code you
should see something like:

hornConfig {files = [tests/pos/skip.js]}

Checking the file : tests/pos/skip.js
Verification: passed

Running All Tests

You can provide any number of files to the verifier. To run a specifc test, write:

$ stack run path/to/file.js

All tests can be found within the `tests` directory.

To run all the positive tests you can write:

$ stack run tests/pos/*

To run all negative tests, you can write:

$ stack run tests/neg/*

Positive tests should give you `Verification: passed`; negative tests should show `Verification: failed`.

Writing Specifications
–

Horn takes specifications in the form of loop invariants, for an example, see `tests/pos/while5.js`

Assignment
–

You need to do three things to complete the assignment.

## Part A: Verification Condition Generation (6 pts)

Fill in the implementation of VC generation by
completing the relevant implementations in:

hw1/src/Horn/Logic/Clauses.hs
hw1/src/Horn/Nano/Nano.hs
hw1/src/Horn/VCGen/VCGen.hs

in particular, wherever it says:

error TODO: FILL THIS IN

In **Clauses.hs** you have to complete functions (1 pt)

subst_exp

which implement substitution, as defined in class; These functions will be useful for implementing the VCGen rule for assignements.

In **Nano.hs**, you have to complete functions (2 pt)

toNanoBexp
toNanoExp
toNanoStmt

These functions translate programs written in ECMAScript (that is, our examples in `tests/pos`, `tests/neg`) into Nano, as defined in this file. The programs are already parsed and in the data-format defined in [this documentation](https://hackage.haskell.org/package/language-ecmascript-0.17.0.1/docs/Language-ECMAScript3-Syntax.html).
You can take a look at the definition of `isNano`, which defines the subset of ECMAScript we want to consider.

To transform While-loops, you can use function **getInvariant s** which extracts invariants specified in the loop body.

You also have to complete functions (1 pt)

expToBase
bexpToBase

which translate program expressions into logic, as define in file `Logic/Clauses.hs`.

File **VCGen.hs** implements verification condition generation based on weakest preconditions, as discussed in class.

You have to fill in function **generateStmtVC** (2 pt). **generateStmtVC**
returns the weakest precondition for the given statement, however, it keeps as
additional state a list of vcs `VCState`, which contains verification conditions
on invariants. You can use functions **getVCs** and **addVCs** to access this

**TIP:** If you dont know what a function in the existing code does, you can
look it up on Hoogle: (https://hoogle.haskell.org/). Hoogle will give you its
type and a link to the documentation.

**NOTE:**You can **only** modify/extend the code in
the functions mentioned above; there is no need to
change any code elsewhere.

## Part B: Verifying A Small Suite of NanoJS Programs (3 pts)

Next, use your implementation to **verify** the suite of programs in

tests/pos/*.js

To do this, you will have to understand the code in order to determine
suitable loop-invariants that you will then put into the .js file.

You can find an example loop invariant in `tests/pos/while5.js`.

Instead of Hoare-triples, Nano contains statements `assume` and `assert`.
`assume(F)` encodes an assumption that formula F holds. `assert(F)` encodes an
obligation to show that formula F holds. In particular a Hoare triple {P} s {Q}
can be translated into

assume(P); s; assert(Q)

As we did not discuss these concepts in class yet, the implementation for these statements is provided.

**Tip** Instead of writing

invariant(P && Q && R);

you can write

invariant(P);
invariant(Q);
invariant(R);

To make sure that your implementation is correct, you also need to make sure that

tests/neg/*.js

do *not* pass verification.

**NOTE:** You can **only** write specification annotations of the form

invariant(p)

That is, you **cannot** add, remove or modify **any** other lines.
(Of course, when **debugging** your specifications, you can make
whatever modifications you like; we just require that the **final**
versions adhere to the above requirement.)

## Part C: Add New Test-cases (1 pt)

Your final assignment is to add 3 new positive test-cases to the folder `tests/pos-new`.
The new test-cases should require non-trivial invariants and pass verification.

CS: assignmentchef QQ: 1823890830 Email: [email protected]