jbranchaud

/*
 * Now that we have an abs function, change the postcondition of method
 * Abs to make use of abs. After confirming the method still verifies,
 * change the body of Abs to also use abs. (After doing this, you will
 * realize there is not much point in having a method that does exactly
 * the same thing as a function method.)
 */
function method abs(x: int): int
{
   if x < 0 then -x else x

jbranchaud

/*
 * Change the loop invariant to 0 <= i <= n+2. Does the loop still verify?
 * Does the assertion i == n after the loop still verify?
 * It no longer verifies because the invariant is no longer sufficient for
 * proving the assertion.
 */
method m(n: nat)
{
   var i: int := 0;
   while (i < n)

jbranchaud

/*
 * With the original loop invariant, change the loop guard from i < n
 * to i != n. Do the loop and the assertion after the loop still verify?
 * Why or why not?
 * It still verifies because the new loop condition doesn't impact the
 * correctness of the assertion.
 */
method m(n: nat)
{
   var i: int := 0;

jbranchaud

/*
 * The ComputeFib method above is more complicated than necessary. Write
 * a simpler program by not introducing a as the Fibonacci number that
 * precedes b, but instead introducing a variable c that succeeds b.
 * Verify your program is correct according to the mathematical definition
 * of Fibonacci.
 */
function fib(n: nat): nat
{
   if n == 0 then 0 else

jbranchaud

function method Fibonacci(n: int): int
  requires n >= 0;
  decreases n;
{
  if n < 2 then n else Fibonacci(n-2) + Fibonacci(n-1)
}

method Testing() {
  assert 0 == Fibonacci(0);
  assert 1 == Fibonacci(1);

jbranchaud

method find(A:array<int>, key: int) returns (k:int)
  requires A != null && A.Length > 0 ;
	requires A[0] < A[A.Length-1] ;
	ensures 0 <= k < A.Length-1 ;
	ensures A[k] < A[k+1] ;
{
	var i:int := 0;
  while(i < A.length) {
    if(A[i] == key) {
      return i;

jbranchaud

/*
 * We are given 3 arrays a,b,c of integers sorted in ascending order, and we are told 
 * that there is a value that occurs in all three arrays. Write a Dafny program to 
 * compute the index in each array where the common value occurs.
 *
 * This is the best implementation I can come up with for this problem, however it
 * is still not verifiable by Dafny. It is a combination of the loop invariants or
 * ensures that seem to fail based on various permutations of saying that p,q,r are
 * < or <= a.Length,b.Length,c.Length, respectively. The long requires statement and
 * the identical assume statement have been added to keep the previously mentioned

jbranchaud

# Some commands from using Soot on the command-line

# First, put the Soot jars on your Java CLASSPATH (preferrably through .bashrc or .zshrc)
export SOOTJAR=path/to/sootclasses-2.5.0.jar
export JASMINJAR=path/to/jasminclasses-2.5.0.jar
export POLYGLOTJAR=path/to/polyglotclasses-1.3.5.jar
export CLASSPATH=$SOOTJAR:$JASMINJAR:$POLYGLOTJAR:$CLASSPATH

# Using Soot to compile a single Java file:
# +-project/

jbranchaud

import java.util.List;

public class GenericsErasure {

	public static void main(String[] args) {
		//...
	}
		
	public static void printList(List list) {
		//...

jbranchaud

import java.util.List;
 
public class ListPrinter {
	
	public static void printList(List<Integer> list) {
		for(Integer i : list) {
  			System.out.println(i.toString()); 
		}
	}