Come up with 2 interesting Alloy formula examples (comparable to examples we have seen in the class):

• one representing valid formula
• one representing invalid formula with a finite counterexample

Explain briefly the results that you obtain when you run the formula in Alloy.

For the valid formula, give a proof why it is valid.

Write an interpreter for our simple programming language extended with assume statement.

The meaning of assignments and control structures is the same as in the usual programming language.

For assume statement, the interpreter should just check whether the condition is true in the current program state. If the condition holds, it should continue. If the condition does not hold, the execution should stop silently.

Use Scala's Int type to represent the unbounded integers in the language.

Your interpreter should take an abstract syntax tree of the program and keep executing the program until it terminates (if it does not terminate, the interpreter should also not terminate). If the program terminates, your interpreter should print the final state of the program.

Here is an example abstract syntax tree that you may wish to use. There is no need to write a parser for this language, you can start from syntax trees. You may modify the syntax tree if needed.

sealed abstract class Term
case class Constant(val c: Int) extends Term
case class Variable(val v: String) extends Term
case class Plus(val t1: Term, val t2: Term) extends Term
case class Minus(val t1: Term, val t2: Term) extends Term
case class Times(val c: Int, val t: Term) extends Term
case class Divide(val t: Term, val c: Int) extends Term
case class Modulo(val t: Term, val c: Int) extends Term
 
sealed abstract class BoolExpr
case class Equal(val t1: Term, val t2: Term) extends BoolExpr
case class LessThan(val t1: Term, val t2: Term) extends BoolExpr
case class GreaterThan(val t1: Term, val t2: Term) extends BoolExpr
case class Negation(val F: BoolExpr) extends BoolExpr
case class And(val f1: BoolExpr, val f2: BoolExpr) extends BoolExpr
case class Or(val f1: BoolExpr, val f2: BoolExpr) extends BoolExpr
 
sealed abstract class Command
case class Assignment(val v: String, val t: Term) extends Command
case class IfThenElse(val cond: BoolExpr, val ifcom: Command, val
elsecom: Command) extends Command
case class Block(val com1: Command, val com2: Command) extends Command
case class WhileLoop( cond: BoolExpr, val com: Command) extends Command

Write syntax tree of a program containing at least two loops and test the execution of your interpreter on this program.

To test the execution, add a 'print' statement that prints a given string and a given integer on the screen.

Using Relational Semantics and the previous syntax tree, write a Scala function that takes

• an assignment statement syntax tree node
• list of all variables that exist in the program

The function should produce a formula describing the relational semantics of the statement.

In the relation, denote the initial value of variable by “old_” prefix, and final value by the variable itself. For example, given statement

x = x + y;

and variables the formula you should obtain should be

Add non-deterministic choice [] to syntax tree, in the form of:

case class Choice(choice1: Command, choice2: Command) extends Command

Use backtracking to execute non-deterministic choice: first execute choice1 and continue program execution, then execute choice2 and continue with program execution.

For example, if the interpreter runs on the syntax tree for the following program

x = 0;
(x = x + 10; [] x = x + 40;)
(x = 2 * x; [] x = 10 * x;)
println("x=", x);

the result should be some permutation of the following four lines:

x=20
x=100
x=80
x=400

That is, each of the four lines must appear in the output exactly once, and no other line should appear.

Write a function that takes program tree with IfThenElse nodes and eliminates IfThenElse by replacing them using Choice and Assume, according to Relational Semantics.

Show an example IfThenElse. Then check that your interpreter gives the same result for IfThenElse and its translation.