jbranchaud

import os
import sys

# add the offending text to file1.txt
f = open("file1.txt", 'r')
content = f.read()
contentArray = content.split('<br />')
for item in contentArray:
    print item
# then copy/paste the console output

jbranchaud

import os

"""
validate_directory: string -> string
given a string that represents a directory, this function will go through and
do some basic validation on it. If there is a problem with the directory as
given, it will be converted to the home directory and returned as is.
"""
def validate_directory(directory=None):
	if directory == None or directory == '~' or not os.path.isdir(directory):

jbranchaud

#!/bin/bash

# the first argument is the string you are looking for --> $1
searchString="$1"

for f in `find . -type f -name "*.java"`
do

    result=`grep "$searchString" $f`

jbranchaud

TYPE

  StrSet         = set(str)
  StrLifted      = lift(StrSet)
  State          = Var -> StrLifted

PROBLEM Constant_Propagation

  direction  : forward
  carrier    : State

jbranchaud

/*
 * Write a method Max that takes two integer parameters and returns
 * their maximum. Add appropriate annotations and make sure  your code
 * verifies.
 */
method Max(a: int, b:int) returns (c: int)
  ensures c >= a && c >= b;
{
  if (a > b) {
    return a;

jbranchaud

/*
 * Write a test method that calls your Max method from
 * Exercise 0 and then asserts something about the result.
 */
method Max(a: int, b:int) returns (c: int)
ensures c >= a && c >= b;
ensures a > b ==> c == a;
ensures a <= b ==> c == b;
{
  if (a > b) {

jbranchaud

/*
 * Using a precondition, change Abs to say it can only be
 * called on negative values. Simplify the body of Abs into
 * just one return statement and make sure the method still
 * verifies.
 */
method Abs(x: int) returns (y: int)
   requires 0 > x;
   ensures 0 <= y;
   ensures 0 <= x ==> x == y;

jbranchaud

/*
 * Keeping the postconditions of Abs the same as above, change
 * the body of Abs to just y := x + 2. What precondition do you
 * need to annotate the method with in order for the verification
 * to go through? What precondition doe you need if the body is
 * y := x + 1? What does that precondition say about when you can
 * call the method?
 */
method Abs(x: int) returns (y: int)
   requires x == -1;

jbranchaud

/*
 * Write a function max that returns the larger of two given
 * integer parameters. Write a test method using an assert that
 * checks that your function is correct.
 */
function max(a: int, b: int): int 
{
   if a > b then a else b
}
method Testing() {

jbranchaud

/*
 * Change your test method from Exercise 4 to capture the value
 * of max to a variable, and then do the checks from Exercise 4
 * using the variable. Dafny will reject this program because you
 * are calling max from real code. Fix this problem using a
 * function method.
 */
function method max(a: int, b: int): int 
{
   if a > b then a else b