# Assignment 2

**Submission Instructions**This assignment is due at 5pm on the date indicated in the class calendar. The starter code for the assignment can be found here (only for problem 2). In order to submit your code, pack your

`Assignment2.js, default.html`

and `question1.sk`

files into a tar file
and submit through stellar.
**Collaboration:** You are allowed to collaborate with one other person for this assignment, but each of you is responsible for submitting your own solution. If you do collaborate with someone else, make sure to name your collaborator in your submission.

If you have any questions, please ask!

## Problem 1 (35 pts)

The goal of this problem is to use Sketch to solve some non-trivial synthesis problem. Your goal for this problem is to synthesize a simple controller for an agent navigating a 2-Dimensional grid. The agent starts at position 0,0, and it's goal is to reach position with coordinates given by`goal`

that
are each between `0`

and `N`

inclusive.
Scattered across the space, however, are some obstacles,
so your goal is to write a controller that moves the agent from its starting point to its
goal without ever landing in a position that includes an obstacle.
Specifically, you must set up a harness that helps you synthesize a function with the following
interface:
`n`

is the number of obstacles in the space`myi`

is the current`i`

coordinate of the agent which needs to be updated by the function.`myj`

is the current`j`

coordinate of the agent which needs to be updated by the function.`obstacles`

is an array with the i and j coordinates of all the obstacles.`goal`

is an array with the i and j coordinates of the goal stored in positions 0 and 1 respectively.

**The specification.**
The goal is to synthesize a control function that satisfies the following constraints.

- Works correctly for between zero and eight obstacles $(0 \leq n < 8)$
- Works correctly for positions of the goal and the obstacles with coordinates in the range $[0, 8)$.
- Can assume that no obstacle is in the goal position or in the start position.
- Can assume that the manhattan distance between any two obstacles is > 3.
- At each step, the controller can add or subtract at most one from each coordinate.
- The position of the agent can never equal the position of one of the obstacles.
- The position of the agent at the end of the process must equal the goal position.
- The agent cannot take more than 24 steps to reach the goal.
- The coordinates of the agent must stay within the range $[0, 8)$

**Clarification:**
The control is not meant to reach the goal in one call. Rather, at each of the
up to 24 steps that the agent is allowed to take, the agent calls the control
to make a move and update its coordinates.
After 24 moves, the agent should be at the goal state.

**The program space.**
The space of programs is given by the following (very stylized) grammar:
`rect`

is listed below.
`let`

as a shorthand notation. Sketch does not actually support a `let`

statement,
so those have to be actual variable declarations.
In order for things to synthesize efficiently,
your generators will have to bound the number of
assignments and the depth of the expression trees.
In order to solve this problem, you
are likely to find the following
flags useful:
`question1.sk`

.

## Part 2 (65 pts)

For this part you will once again be working in JavaScript. The goal of the second problem will be to synthesize invariants necessary to prove that a piece of code is correct. We will be working in the context of a very simple language involving variables, simple arithmetic operations, and a set of simple commands (if, while, assignment and sequential composition). You will implement this in two parts, first, you will generate the verification condition as an AST using the same AST nodes provided to you for representing the program, and then you will generate sketch code from this AST.
**a) VC as an AST:**
For this part, you may need to introduce additional AST nodes in order to represent the unknown invariants and to indicate the variables that may be used by this. Other than that, this should be a relatively straightforward implementation of verification condition generation.

**b) VC as a sketch:**
For the second part, you will need to pretty-print your VC as a sketch so that we can rely on the
sketch synthesizer to discover loop invariants for us. If you like, you can write your generators
as a separate library that is included by your generated sketch, although you may do better by
creating specialized generators based on what you observe in the program.
The sketch should have a function named `invariant_i`

for each loop in the program
to help identify the loop invariants.

**c) Test cases:**
You need to submit five test cases for which your system can generate interesting invariants.

## Graduate Credit

If you are taking the class for graduate credit, you must also implement the following to get full credit for Part 2. If you are taking the class for undergraduate credit, you can complete this problem for 10 points of extra credit.
For this part, you should extend your solution to part2 to support linear expression holes
as part of the input program. The hole should resolve to a linear expression of a subset
of the variables present in the program.
Your goal is to synthesize expressions for these holes such that the program verifies **and terminates**.