Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

10 files changed, 958 insertions, 958 deletions

diff --git a/Source/Forro/Ast.fs b/Source/Forro/Ast.fs
index 6c7ba65c..779beefb 100644
--- a/Source/Forro/Ast.fs
+++ b/Source/Forro/Ast.fs
@@ -1,38 +1,38 @@
-module Forro

-

-type Field = Head | Tail | Valid

-

-type Variable = Var of string

-

-let VarName v =

-    match v with Var(x) -> x

-

-type Operator = Eq | Neq | Plus | Minus | Times

-              | Less | AtMost | And | Or

-

-type Expression =

-    | Constant of int

-    | Null

-    | Identifier of Variable

-    | Not of Expression

-    | Binary of Operator * Expression * Expression

-    | Select of Expression * Field

-    | Old of Expression

-

-type Statement =

-    | Assign of Variable * Expression

-    | Update of Expression * Field * Expression

-    | Alloc of Variable * Expression * Expression

-    | IfStmt of Expression * StmtList * StmtList

-    | WhileStmt of Expression * Expression list * StmtList

-    | CallStmt of Variable list * string * Expression list

-    | Assert of Expression

-

-and StmtList  =

-    Block of Statement list

-

-type Procedure =

-    Proc of string * Variable list * Variable list * Expression * Expression * StmtList

-

-type Program =

-    Prog of Procedure list

+module Forro
+
+type Field = Head | Tail | Valid
+
+type Variable = Var of string
+
+let VarName v =
+    match v with Var(x) -> x
+
+type Operator = Eq | Neq | Plus | Minus | Times
+              | Less | AtMost | And | Or
+
+type Expression =
+    | Constant of int
+    | Null
+    | Identifier of Variable
+    | Not of Expression
+    | Binary of Operator * Expression * Expression
+    | Select of Expression * Field
+    | Old of Expression
+
+type Statement =
+    | Assign of Variable * Expression
+    | Update of Expression * Field * Expression
+    | Alloc of Variable * Expression * Expression
+    | IfStmt of Expression * StmtList * StmtList
+    | WhileStmt of Expression * Expression list * StmtList
+    | CallStmt of Variable list * string * Expression list
+    | Assert of Expression
+
+and StmtList  =
+    Block of Statement list
+
+type Procedure =
+    Proc of string * Variable list * Variable list * Expression * Expression * StmtList
+
+type Program =
+    Prog of Procedure list
diff --git a/Source/Forro/BoogieAst.fs b/Source/Forro/BoogieAst.fs
index 964f6667..7c1819da 100644
--- a/Source/Forro/BoogieAst.fs
+++ b/Source/Forro/BoogieAst.fs
@@ -1,40 +1,40 @@
-namespace BoogieAst

-

-type BType = BInt | BBool

-

-type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr

-

-type BExpression =

-    | BConstant of int

-    | BFalse

-    | BTrue

-    | BNull

-    | BIdentifier of string

-    | BNot of BExpression

-    | BBinary of BOperator * BExpression * BExpression

-    | BSelect of string * BExpression

-    | BToPred of BExpression    // BToPred(e) == (e != 0)

-    | BToTerm of BExpression    // BToTerm(e) == (if e then 1 else 0)

-    | BOld of BExpression

-    | BFunc of string * BExpression list

-

-type BStmtList  =

-    BBlock of Statement list

-

-and Statement =

-    | BAssign of string * BExpression

-    | BUpdate of string * BExpression * BExpression

-    | BHavoc of string list

-    | BAssert of BExpression

-    | BAssume of BExpression

-    | BIfStmt of BExpression * BStmtList * BStmtList

-    | BWhileStmt of BExpression * BExpression list * BStmtList

-    | BCallStmt of string list * string * BExpression list

-

-type BVarDecl = BVar of string * BType

-

-type BProcedure =

-    BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList

-

-type BProgram =

-    BProg of string * BProcedure list

+namespace BoogieAst
+
+type BType = BInt | BBool
+
+type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr
+
+type BExpression =
+    | BConstant of int
+    | BFalse
+    | BTrue
+    | BNull
+    | BIdentifier of string
+    | BNot of BExpression
+    | BBinary of BOperator * BExpression * BExpression
+    | BSelect of string * BExpression
+    | BToPred of BExpression    // BToPred(e) == (e != 0)
+    | BToTerm of BExpression    // BToTerm(e) == (if e then 1 else 0)
+    | BOld of BExpression
+    | BFunc of string * BExpression list
+
+type BStmtList  =
+    BBlock of Statement list
+
+and Statement =
+    | BAssign of string * BExpression
+    | BUpdate of string * BExpression * BExpression
+    | BHavoc of string list
+    | BAssert of BExpression
+    | BAssume of BExpression
+    | BIfStmt of BExpression * BStmtList * BStmtList
+    | BWhileStmt of BExpression * BExpression list * BStmtList
+    | BCallStmt of string list * string * BExpression list
+
+type BVarDecl = BVar of string * BType
+
+type BProcedure =
+    BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList
+
+type BProgram =
+    BProg of string * BProcedure list
diff --git a/Source/Forro/BoogiePrinter.fs b/Source/Forro/BoogiePrinter.fs
index 8f2b37ee..e9497ab5 100644
--- a/Source/Forro/BoogiePrinter.fs
+++ b/Source/Forro/BoogiePrinter.fs
@@ -1,112 +1,112 @@
-module BoogiePrinter

-

-open ForroPrinter  // to get Indent

-open BoogieAst

-

-let PrintWithSep Pr sep list =

-    ignore (List.fold (fun sp e -> printf "%s" sp ; Pr e ; sep) "" list)

-

-let TypeName t =

-    match t with

-    | BInt -> "int"

-    | BBool -> "bool"

-

-let PrVarType v =

-    match v with

-    | BVar(name,t) ->

-        printf "%s: %s" name (TypeName t)

-

-let PrintOp op =

-    printf " "

-    match op with

-    | BEq -> printf "=="

-    | BNeq -> printf "!="

-    | BPlus -> printf "+"

-    | BMinus -> printf "-"

-    | BTimes -> printf "*"

-    | BLess -> printf "<"

-    | BAtMost -> printf "<="

-    | BAnd -> printf "&&"

-    | BOr -> printf "||"

-    printf " "

-

-let rec PrintExpr e =

-    match e with

-    | BConstant(x) -> printf "%d" x

-    | BFalse -> printf "false"

-    | BTrue -> printf "true"

-    | BNull -> printf "null"

-    | BIdentifier(id) -> printf "%s" id

-    | BNot(e) -> printf "!(" ; PrintExpr e ; printf ")"

-    | BBinary(op,e0,e1) -> printf "(" ; PrintExpr e0 ; PrintOp op ; PrintExpr e1 ; printf ")"

-    | BSelect(var,e) -> printf "%s[" var ; PrintExpr e ; printf "]"

-    | BToPred(e) -> printf "(" ; PrintExpr e ; printf " != 0)"

-    | BToTerm(e) -> printf "(if " ; PrintExpr e ; printf " then 1 else 0)"

-    | BOld(e) -> printf "old(" ; PrintExpr e ; printf ")"

-    | BFunc(id,args) -> printf "%s(" id ; PrintWithSep PrintExpr ", " args ; printf ")"

-

-let rec PrintStmt indent stmt =

-    Indent indent

-    let ind = indent + 2

-    match stmt with

-    | BAssign(id,e) -> printf "%s := " id ; PrintExpr e ; printfn ";"

-    | BUpdate(id,obj,rhs) -> printf "%s[" id ; PrintExpr obj ; printf "] := " ; PrintExpr rhs ; printfn ";"

-    | BHavoc(ids) -> printf "havoc " ; PrintWithSep (printf "%s") ", " ids ; printfn ";"

-    | BAssert(e) -> printf "assert " ; PrintExpr e ; printfn ";"

-    | BAssume(e) -> printf "assume " ; PrintExpr e ; printfn ";"

-    | BIfStmt(e,thn,els) ->

-        printf "if (" ; PrintExpr e ; printfn ") {"

-        PrintStmtList ind thn

-        Indent indent

-        printfn "} else {"

-        PrintStmtList ind els

-        Indent indent

-        printfn "}"

-    | BWhileStmt(e, invs, body) ->

-        printf "while (" ; PrintExpr e ; printfn ")"

-        List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv ; printfn ";") invs

-        Indent indent

-        printfn "{"

-        PrintStmtList ind body

-        Indent indent

-        printfn "}"

-    | BCallStmt(outs, id, ins) ->

-        printf "call "

-        if outs.IsEmpty then () else PrintWithSep (fun p -> printf "%s" p) ", " outs ; printf " := "

-        printf "%s(" id

-        PrintWithSep PrintExpr ", " ins

-        printfn ");"

-

-and PrintStmtList indent stmts =

-    match stmts with

-    | BBlock(slist) -> List.iter (fun s -> PrintStmt indent s) slist

-

-let BPrintProc proc =

-    match proc with

-    | BProc(name, ins, outs, req, frame, ens, locals, body) ->

-        printfn ""

-        printf "procedure %s(" name

-        PrintWithSep PrVarType ", " ins

-        printf ") returns ("

-        PrintWithSep PrVarType ", " outs

-        printfn ")"

-        printf "  requires "

-        PrintExpr req

-        printfn ";"

-        printf "  modifies "

-        PrintWithSep (printf "%s") ", " frame

-        printfn ";"

-        printf "  ensures "

-        PrintExpr ens

-        printfn ";"

-        printfn "{"

-        List.iter (fun local -> printf "  var " ; PrVarType local ; printfn ";") locals

-        if locals.IsEmpty then () else printfn ""

-        PrintStmtList 2 body

-        printfn "}"

-

-let BPrint (prog: BProgram) =

-    match prog with

-    | BProg(prelude, procs) ->

-        printfn "%s" prelude

-        List.iter BPrintProc procs

+module BoogiePrinter
+
+open ForroPrinter  // to get Indent
+open BoogieAst
+
+let PrintWithSep Pr sep list =
+    ignore (List.fold (fun sp e -> printf "%s" sp ; Pr e ; sep) "" list)
+
+let TypeName t =
+    match t with
+    | BInt -> "int"
+    | BBool -> "bool"
+
+let PrVarType v =
+    match v with
+    | BVar(name,t) ->
+        printf "%s: %s" name (TypeName t)
+
+let PrintOp op =
+    printf " "
+    match op with
+    | BEq -> printf "=="
+    | BNeq -> printf "!="
+    | BPlus -> printf "+"
+    | BMinus -> printf "-"
+    | BTimes -> printf "*"
+    | BLess -> printf "<"
+    | BAtMost -> printf "<="
+    | BAnd -> printf "&&"
+    | BOr -> printf "||"
+    printf " "
+
+let rec PrintExpr e =
+    match e with
+    | BConstant(x) -> printf "%d" x
+    | BFalse -> printf "false"
+    | BTrue -> printf "true"
+    | BNull -> printf "null"
+    | BIdentifier(id) -> printf "%s" id
+    | BNot(e) -> printf "!(" ; PrintExpr e ; printf ")"
+    | BBinary(op,e0,e1) -> printf "(" ; PrintExpr e0 ; PrintOp op ; PrintExpr e1 ; printf ")"
+    | BSelect(var,e) -> printf "%s[" var ; PrintExpr e ; printf "]"
+    | BToPred(e) -> printf "(" ; PrintExpr e ; printf " != 0)"
+    | BToTerm(e) -> printf "(if " ; PrintExpr e ; printf " then 1 else 0)"
+    | BOld(e) -> printf "old(" ; PrintExpr e ; printf ")"
+    | BFunc(id,args) -> printf "%s(" id ; PrintWithSep PrintExpr ", " args ; printf ")"
+
+let rec PrintStmt indent stmt =
+    Indent indent
+    let ind = indent + 2
+    match stmt with
+    | BAssign(id,e) -> printf "%s := " id ; PrintExpr e ; printfn ";"
+    | BUpdate(id,obj,rhs) -> printf "%s[" id ; PrintExpr obj ; printf "] := " ; PrintExpr rhs ; printfn ";"
+    | BHavoc(ids) -> printf "havoc " ; PrintWithSep (printf "%s") ", " ids ; printfn ";"
+    | BAssert(e) -> printf "assert " ; PrintExpr e ; printfn ";"
+    | BAssume(e) -> printf "assume " ; PrintExpr e ; printfn ";"
+    | BIfStmt(e,thn,els) ->
+        printf "if (" ; PrintExpr e ; printfn ") {"
+        PrintStmtList ind thn
+        Indent indent
+        printfn "} else {"
+        PrintStmtList ind els
+        Indent indent
+        printfn "}"
+    | BWhileStmt(e, invs, body) ->
+        printf "while (" ; PrintExpr e ; printfn ")"
+        List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv ; printfn ";") invs
+        Indent indent
+        printfn "{"
+        PrintStmtList ind body
+        Indent indent
+        printfn "}"
+    | BCallStmt(outs, id, ins) ->
+        printf "call "
+        if outs.IsEmpty then () else PrintWithSep (fun p -> printf "%s" p) ", " outs ; printf " := "
+        printf "%s(" id
+        PrintWithSep PrintExpr ", " ins
+        printfn ");"
+
+and PrintStmtList indent stmts =
+    match stmts with
+    | BBlock(slist) -> List.iter (fun s -> PrintStmt indent s) slist
+
+let BPrintProc proc =
+    match proc with
+    | BProc(name, ins, outs, req, frame, ens, locals, body) ->
+        printfn ""
+        printf "procedure %s(" name
+        PrintWithSep PrVarType ", " ins
+        printf ") returns ("
+        PrintWithSep PrVarType ", " outs
+        printfn ")"
+        printf "  requires "
+        PrintExpr req
+        printfn ";"
+        printf "  modifies "
+        PrintWithSep (printf "%s") ", " frame
+        printfn ";"
+        printf "  ensures "
+        PrintExpr ens
+        printfn ";"
+        printfn "{"
+        List.iter (fun local -> printf "  var " ; PrVarType local ; printfn ";") locals
+        if locals.IsEmpty then () else printfn ""
+        PrintStmtList 2 body
+        printfn "}"
+
+let BPrint (prog: BProgram) =
+    match prog with
+    | BProg(prelude, procs) ->
+        printfn "%s" prelude
+        List.iter BPrintProc procs
diff --git a/Source/Forro/Forro.fsproj b/Source/Forro/Forro.fsproj
index 8f6fc223..161d79db 100644
--- a/Source/Forro/Forro.fsproj
+++ b/Source/Forro/Forro.fsproj
@@ -1,83 +1,83 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

-  <PropertyGroup>

-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">x86</Platform>

-    <ProductVersion>8.0.30703</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{c75e47a0-e88d-4035-9ebf-f6647af92b79}</ProjectGuid>

-    <OutputType>Exe</OutputType>

-    <RootNamespace>Language</RootNamespace>

-    <AssemblyName>Forro</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <TargetFrameworkProfile>Client</TargetFrameworkProfile>

-    <Name>Language</Name>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <Tailcalls>false</Tailcalls>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <WarningLevel>3</WarningLevel>

-    <PlatformTarget>x86</PlatformTarget>

-    <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <Tailcalls>true</Tailcalls>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <WarningLevel>3</WarningLevel>

-    <PlatformTarget>x86</PlatformTarget>

-    <DocumentationFile>bin\Release\Language.XML</DocumentationFile>

-  </PropertyGroup>

-  <Import Project="$(MSBuildExtensionsPath32)\..\Microsoft F#\v4.0\Microsoft.FSharp.Targets" />

-  <Import Project="$(MSBuildExtensionsPath32)\..\FSharpPowerPack-2.0.0.0\bin\FSharp.PowerPack.targets" />

-  <PropertyGroup>

-    <FsLexOutputFolder>$(IntermediateOutputPath)</FsLexOutputFolder>

-    <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>

-  </PropertyGroup>

-  <ItemGroup>

-    <Compile Include="Ast.fs" />

-    <Compile Include="$(IntermediateOutputPath)\Parser.fs">

-      <Visible>false</Visible>

-      <Link>Parser.fs</Link>

-    </Compile>

-    <Compile Include="$(IntermediateOutputPath)\Lexer.fs">

-      <Visible>false</Visible>

-      <Link>Lexer.fs</Link>

-    </Compile>

-    <FsYacc Include="Parser.fsy">

-      <OtherFlags>--module Parser</OtherFlags>

-    </FsYacc>

-    <FsLex Include="Lexer.fsl">

-      <OtherFlags>--unicode</OtherFlags>

-    </FsLex>

-    <Compile Include="Printer.fs" />

-    <Compile Include="Resolver.fs" />

-    <Compile Include="BoogieAst.fs" />

-    <Compile Include="BoogiePrinter.fs" />

-    <Compile Include="Translator.fs" />

-    <Compile Include="Main.fs" />

-  </ItemGroup>

-  <ItemGroup>

-    <Reference Include="FSharp.PowerPack">

-      <HintPath>C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll</HintPath>

-    </Reference>

-    <Reference Include="mscorlib" />

-    <Reference Include="FSharp.Core" />

-    <Reference Include="System" />

-    <Reference Include="System.Core" />

-    <Reference Include="System.Numerics" />

-  </ItemGroup>

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

-       Other similar extension points exist, see Microsoft.Common.targets.

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
+    <ProductVersion>8.0.30703</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{c75e47a0-e88d-4035-9ebf-f6647af92b79}</ProjectGuid>
+    <OutputType>Exe</OutputType>
+    <RootNamespace>Language</RootNamespace>
+    <AssemblyName>Forro</AssemblyName>
+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+    <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+    <Name>Language</Name>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <Tailcalls>false</Tailcalls>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <WarningLevel>3</WarningLevel>
+    <PlatformTarget>x86</PlatformTarget>
+    <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <Tailcalls>true</Tailcalls>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <WarningLevel>3</WarningLevel>
+    <PlatformTarget>x86</PlatformTarget>
+    <DocumentationFile>bin\Release\Language.XML</DocumentationFile>
+  </PropertyGroup>
+  <Import Project="$(MSBuildExtensionsPath32)\..\Microsoft F#\v4.0\Microsoft.FSharp.Targets" />
+  <Import Project="$(MSBuildExtensionsPath32)\..\FSharpPowerPack-2.0.0.0\bin\FSharp.PowerPack.targets" />
+  <PropertyGroup>
+    <FsLexOutputFolder>$(IntermediateOutputPath)</FsLexOutputFolder>
+    <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
+  </PropertyGroup>
+  <ItemGroup>
+    <Compile Include="Ast.fs" />
+    <Compile Include="$(IntermediateOutputPath)\Parser.fs">
+      <Visible>false</Visible>
+      <Link>Parser.fs</Link>
+    </Compile>
+    <Compile Include="$(IntermediateOutputPath)\Lexer.fs">
+      <Visible>false</Visible>
+      <Link>Lexer.fs</Link>
+    </Compile>
+    <FsYacc Include="Parser.fsy">
+      <OtherFlags>--module Parser</OtherFlags>
+    </FsYacc>
+    <FsLex Include="Lexer.fsl">
+      <OtherFlags>--unicode</OtherFlags>
+    </FsLex>
+    <Compile Include="Printer.fs" />
+    <Compile Include="Resolver.fs" />
+    <Compile Include="BoogieAst.fs" />
+    <Compile Include="BoogiePrinter.fs" />
+    <Compile Include="Translator.fs" />
+    <Compile Include="Main.fs" />
+  </ItemGroup>
+  <ItemGroup>
+    <Reference Include="FSharp.PowerPack">
+      <HintPath>C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll</HintPath>
+    </Reference>
+    <Reference Include="mscorlib" />
+    <Reference Include="FSharp.Core" />
+    <Reference Include="System" />
+    <Reference Include="System.Core" />
+    <Reference Include="System.Numerics" />
+  </ItemGroup>
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
 </Project>
\ No newline at end of file
diff --git a/Source/Forro/Lexer.fsl b/Source/Forro/Lexer.fsl
index 4252af23..5f69df7c 100644
--- a/Source/Forro/Lexer.fsl
+++ b/Source/Forro/Lexer.fsl
@@ -1,60 +1,60 @@
-{

-module Lexer

-open System

-open Parser

-open Microsoft.FSharp.Text.Lexing

-}

-

-// These are some regular expression definitions

-let digit = ['0'-'9']

-let nondigit = [ 'a'-'z' 'A'-'Z' '_' ]

-let idchar = (nondigit | digit)

-let whitespace = [' ' '\t' ]

-let newline = ('\n' | '\r' '\n')

-

-rule tokenize = parse

-| whitespace    { tokenize lexbuf }

-| newline       { // lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos() ; 

-                  tokenize lexbuf }

-// operators

-| "=="          { EQ }

-| "!="          { NEQ }

-| "+"           { PLUS }

-| "-"           { MINUS }

-| "*"           { STAR }

-| "<"           { LESS }

-| "<="          { ATMOST }

-| "and"         { AND }

-| "or"          { OR }

-| "not"         { NOT }

-| "old"         { OLD }

-| "."           { DOT }

-// misc

-| "("           { LPAREN }

-| ")"           { RPAREN }

-| "{"           { LCURLY }

-| "}"           { RCURLY }

-| ";"           { SEMI }

-| ","           { COMMA }

-| ":="          { ASSIGN }

-// keywords

-| "procedure"   { PROCEDURE }

-| "requires"    { REQUIRES }

-| "ensures"     { ENSURES }

-| "do"          { DO }

-| "end"         { END }

-| "new"         { NEW }

-| "if"          { IF }

-| "then"        { THEN }

-| "else"        { ELSE }

-| "while"       { WHILE }

-| "invariant"   { INVARIANT }

-| "call"        { CALL }

-| "assert"      { ASSERT }

-// literals

-| ['-']?digit+  { INT32 (Int32.Parse(LexBuffer<char>.LexemeString lexbuf)) }

-| "null"        { NULL }

-// identifiers

-| idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }

-// EOF

-| eof   { EOF }

+{
+module Lexer
+open System
+open Parser
+open Microsoft.FSharp.Text.Lexing
+}
+
+// These are some regular expression definitions
+let digit = ['0'-'9']
+let nondigit = [ 'a'-'z' 'A'-'Z' '_' ]
+let idchar = (nondigit | digit)
+let whitespace = [' ' '\t' ]
+let newline = ('\n' | '\r' '\n')
+
+rule tokenize = parse
+| whitespace    { tokenize lexbuf }
+| newline       { // lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos() ; 
+                  tokenize lexbuf }
+// operators
+| "=="          { EQ }
+| "!="          { NEQ }
+| "+"           { PLUS }
+| "-"           { MINUS }
+| "*"           { STAR }
+| "<"           { LESS }
+| "<="          { ATMOST }
+| "and"         { AND }
+| "or"          { OR }
+| "not"         { NOT }
+| "old"         { OLD }
+| "."           { DOT }
+// misc
+| "("           { LPAREN }
+| ")"           { RPAREN }
+| "{"           { LCURLY }
+| "}"           { RCURLY }
+| ";"           { SEMI }
+| ","           { COMMA }
+| ":="          { ASSIGN }
+// keywords
+| "procedure"   { PROCEDURE }
+| "requires"    { REQUIRES }
+| "ensures"     { ENSURES }
+| "do"          { DO }
+| "end"         { END }
+| "new"         { NEW }
+| "if"          { IF }
+| "then"        { THEN }
+| "else"        { ELSE }
+| "while"       { WHILE }
+| "invariant"   { INVARIANT }
+| "call"        { CALL }
+| "assert"      { ASSERT }
+// literals
+| ['-']?digit+  { INT32 (Int32.Parse(LexBuffer<char>.LexemeString lexbuf)) }
+| "null"        { NULL }
+// identifiers
+| idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }
+// EOF
+| eof   { EOF }
diff --git a/Source/Forro/Main.fs b/Source/Forro/Main.fs
index 3b0f550f..07d1a12e 100644
--- a/Source/Forro/Main.fs
+++ b/Source/Forro/Main.fs
@@ -1,57 +1,57 @@
-open System

-open Microsoft.FSharp.Text.Lexing

-

-open System.IO

-

-open ForroPrinter

-open Resolver

-open Lexer

-open Parser

-open BoogiePrinter

-

-open Translator

-

-let readAndProcess tracing (filename: string) =

-    try

-        if tracing then printfn "Forró: version 1.0" else ()

-        // lex

-        let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader

-        let lexbuf = LexBuffer<char>.FromTextReader(f)

-        lexbuf.EndPos <- { pos_bol = 0;

-                           pos_fname=if filename = null then "stdin" else filename; 

-                           pos_cnum=0;

-                           pos_lnum=1 }

-        // parse

-        let prog = Parser.start Lexer.tokenize lexbuf

-        // print the given Forró program

-        if tracing then

-            printfn "---------- Given Forró program ----------"

-            Print prog

-        else ()

-        // make sure the program is legal

-        let rprog = Resolve prog

-        // translate into Boogie

-        let bprog = Translate rprog

-        // print the Boogie program

-        if tracing then printfn "---------- Resulting Boogie program ----------" else ()

-        BPrint bprog

-        // that's it

-        if tracing then printfn "----------" ; printfn "Done" else ()

-

-    with

-     | ResolutionError(msg) ->

-        printfn "Resolution error: %s" msg            

-     | ex ->

-        printfn "Unhandled Exception: %s" ex.Message

-

-let rec start n (args: string []) tracing filename =

-  if n < args.Length then

-    let arg = args.[n]

-    if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()

-    let filename = if arg.StartsWith "/" then filename else arg

-    start (n+1) args (tracing || arg = "/trace") filename

-  else

-    readAndProcess tracing filename

-

-let args = Environment.GetCommandLineArgs()

-start 1 args false null

+open System
+open Microsoft.FSharp.Text.Lexing
+
+open System.IO
+
+open ForroPrinter
+open Resolver
+open Lexer
+open Parser
+open BoogiePrinter
+
+open Translator
+
+let readAndProcess tracing (filename: string) =
+    try
+        if tracing then printfn "Forró: version 1.0" else ()
+        // lex
+        let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
+        let lexbuf = LexBuffer<char>.FromTextReader(f)
+        lexbuf.EndPos <- { pos_bol = 0;
+                           pos_fname=if filename = null then "stdin" else filename; 
+                           pos_cnum=0;
+                           pos_lnum=1 }
+        // parse
+        let prog = Parser.start Lexer.tokenize lexbuf
+        // print the given Forró program
+        if tracing then
+            printfn "---------- Given Forró program ----------"
+            Print prog
+        else ()
+        // make sure the program is legal
+        let rprog = Resolve prog
+        // translate into Boogie
+        let bprog = Translate rprog
+        // print the Boogie program
+        if tracing then printfn "---------- Resulting Boogie program ----------" else ()
+        BPrint bprog
+        // that's it
+        if tracing then printfn "----------" ; printfn "Done" else ()
+
+    with
+     | ResolutionError(msg) ->
+        printfn "Resolution error: %s" msg            
+     | ex ->
+        printfn "Unhandled Exception: %s" ex.Message
+
+let rec start n (args: string []) tracing filename =
+  if n < args.Length then
+    let arg = args.[n]
+    if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()
+    let filename = if arg.StartsWith "/" then filename else arg
+    start (n+1) args (tracing || arg = "/trace") filename
+  else
+    readAndProcess tracing filename
+
+let args = Environment.GetCommandLineArgs()
+start 1 args false null
diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy
index 5dbb8a4c..af64d267 100644
--- a/Source/Forro/Parser.fsy
+++ b/Source/Forro/Parser.fsy
@@ -1,122 +1,122 @@
-%{

-

-open Forro

-

-exception ParseError of string

-

-let StringsToVariables ss = [ for s in ss -> Var(s) ]

-

-let IdToField id =

-    match id with

-    | "head" -> Field.Head

-    | "tail" -> Field.Tail

-    | "valid" -> Field.Valid

-    | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')"))

-

-%}

-

-// The start token becomes a parser function in the compiled code:

-%start start

-

-// These are the terminal tokens of the grammar along with the types of

-// the data carried by each token:

-%token <string> ID

-%token <System.Int32> INT32

-%token NULL

-%token DOT

-%token NOT

-%token STAR

-%token PLUS MINUS

-%token EQ NEQ LESS ATMOST

-%token AND OR

-%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA ASSIGN

-%token PROCEDURE REQUIRES ENSURES DO END

-%token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT

-%token EOF

-

-// This is the type of the data produced by a successful reduction of the 'start'

-// symbol:

-%type < Forro.Program > start

-

-%%

-

-// These are the rules of the grammar along with the F# code of the 

-// actions executed as rules are reduced.  In this case the actions 

-// produce data using F# data construction terms.

-start: Prog EOF { Prog(List.rev($1)) }

-

-Prog: Proc { [$1] }

-    | Prog Proc { $2 :: $1  }

-

-Proc:

-    PROCEDURE Signature ProcedureSpec

-    DO StmtList END SEMI

-    { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) }

-

-ProcedureSpec:

-      REQUIRES Expression ENSURES Expression { $2, $4 }

-

-Signature:

-      ID LPAREN IdList RPAREN                { [], $1, $3 }

-    | ID LPAREN RPAREN                       { [], $1, [] }

-    | IdList ASSIGN ID LPAREN IdList RPAREN  { $1, $3, $5 }

-    | IdList ASSIGN ID LPAREN RPAREN         { $1, $3, [] }

-

-IdList: ID      { [$1] }

-    | ID COMMA IdList { $1 :: $3 }

-

-Expression:

-      AtomicExpr { $1 }

-    | NOT Expression { Not($2) }

-    | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) }

-    | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) }

-    | Expression STAR Expression { Binary(Operator.Times, $1, $3) }

-    | Expression EQ Expression { Binary(Operator.Eq, $1, $3) }

-    | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) }

-    | Expression LESS Expression { Binary(Operator.Less, $1, $3) }

-    | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) }

-    | Expression AND Expression { Binary(Operator.And, $1, $3) }

-    | Expression OR Expression { Binary(Operator.Or, $1, $3) }

-

-AtomicExpr:

-      INT32         { Constant($1) }

-    | NULL          { Null }

-    | ID            { Identifier(Var($1)) }

-    | OLD LPAREN Expression RPAREN { Old($3) }

-    | LPAREN Expression RPAREN { $2 }

-    | FieldSelect { match $1 with e,f -> Select(e,f) }

-

-FieldSelect:

-    AtomicExpr DOT ID { $1, IdToField $3 }

-

-ExprList:

-    | Expression                { [$1] }

-    | Expression COMMA ExprList { $1::$3 }

-

-VarList:

-    | ID ASSIGN        { [Var($1)] }

-    | ID COMMA VarList { Var($1)::$3 }

-

-StmtList:

-    StmtListX  { Block($1) }

-

-StmtListX:

-                     { [] }

-    | Stmt StmtListX { $1::$2 }

-

-Stmt:

-      ID ASSIGN Expression SEMI                           { Assign(Var($1), $3) }

-    | ID ASSIGN NEW LPAREN Expression COMMA

-                    Expression RPAREN SEMI                { Alloc(Var($1), $5, $7) }

-    | FieldSelect ASSIGN Expression SEMI                  { match $1 with e,f -> Update(e, f, $3) }

-    | IF Expression THEN StmtList ELSE StmtList END SEMI  { IfStmt($2,$4,$6) }

-    | WHILE Expression Invariants DO StmtList END SEMI    { WhileStmt($2,$3,$5) }

-    | CALL ID LPAREN RPAREN SEMI                          { CallStmt([],$2,[]) }

-    | CALL ID LPAREN ExprList RPAREN SEMI                 { CallStmt([],$2,$4) }

-    | CALL VarList ID LPAREN RPAREN SEMI                  { CallStmt($2,$3,[]) }

-    | CALL VarList ID LPAREN ExprList RPAREN SEMI         { CallStmt($2,$3,$5) }

-    | ASSERT Expression SEMI                              { Assert($2) }

-

-Invariants:

-                                       { [] }

-    | INVARIANT Expression Invariants  { $2::$3 }

+%{
+
+open Forro
+
+exception ParseError of string
+
+let StringsToVariables ss = [ for s in ss -> Var(s) ]
+
+let IdToField id =
+    match id with
+    | "head" -> Field.Head
+    | "tail" -> Field.Tail
+    | "valid" -> Field.Valid
+    | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')"))
+
+%}
+
+// The start token becomes a parser function in the compiled code:
+%start start
+
+// These are the terminal tokens of the grammar along with the types of
+// the data carried by each token:
+%token <string> ID
+%token <System.Int32> INT32
+%token NULL
+%token DOT
+%token NOT
+%token STAR
+%token PLUS MINUS
+%token EQ NEQ LESS ATMOST
+%token AND OR
+%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA ASSIGN
+%token PROCEDURE REQUIRES ENSURES DO END
+%token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT
+%token EOF
+
+// This is the type of the data produced by a successful reduction of the 'start'
+// symbol:
+%type < Forro.Program > start
+
+%%
+
+// These are the rules of the grammar along with the F# code of the 
+// actions executed as rules are reduced.  In this case the actions 
+// produce data using F# data construction terms.
+start: Prog EOF { Prog(List.rev($1)) }
+
+Prog: Proc { [$1] }
+    | Prog Proc { $2 :: $1  }
+
+Proc:
+    PROCEDURE Signature ProcedureSpec
+    DO StmtList END SEMI
+    { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) }
+
+ProcedureSpec:
+      REQUIRES Expression ENSURES Expression { $2, $4 }
+
+Signature:
+      ID LPAREN IdList RPAREN                { [], $1, $3 }
+    | ID LPAREN RPAREN                       { [], $1, [] }
+    | IdList ASSIGN ID LPAREN IdList RPAREN  { $1, $3, $5 }
+    | IdList ASSIGN ID LPAREN RPAREN         { $1, $3, [] }
+
+IdList: ID      { [$1] }
+    | ID COMMA IdList { $1 :: $3 }
+
+Expression:
+      AtomicExpr { $1 }
+    | NOT Expression { Not($2) }
+    | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) }
+    | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) }
+    | Expression STAR Expression { Binary(Operator.Times, $1, $3) }
+    | Expression EQ Expression { Binary(Operator.Eq, $1, $3) }
+    | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) }
+    | Expression LESS Expression { Binary(Operator.Less, $1, $3) }
+    | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) }
+    | Expression AND Expression { Binary(Operator.And, $1, $3) }
+    | Expression OR Expression { Binary(Operator.Or, $1, $3) }
+
+AtomicExpr:
+      INT32         { Constant($1) }
+    | NULL          { Null }
+    | ID            { Identifier(Var($1)) }
+    | OLD LPAREN Expression RPAREN { Old($3) }
+    | LPAREN Expression RPAREN { $2 }
+    | FieldSelect { match $1 with e,f -> Select(e,f) }
+
+FieldSelect:
+    AtomicExpr DOT ID { $1, IdToField $3 }
+
+ExprList:
+    | Expression                { [$1] }
+    | Expression COMMA ExprList { $1::$3 }
+
+VarList:
+    | ID ASSIGN        { [Var($1)] }
+    | ID COMMA VarList { Var($1)::$3 }
+
+StmtList:
+    StmtListX  { Block($1) }
+
+StmtListX:
+                     { [] }
+    | Stmt StmtListX { $1::$2 }
+
+Stmt:
+      ID ASSIGN Expression SEMI                           { Assign(Var($1), $3) }
+    | ID ASSIGN NEW LPAREN Expression COMMA
+                    Expression RPAREN SEMI                { Alloc(Var($1), $5, $7) }
+    | FieldSelect ASSIGN Expression SEMI                  { match $1 with e,f -> Update(e, f, $3) }
+    | IF Expression THEN StmtList ELSE StmtList END SEMI  { IfStmt($2,$4,$6) }
+    | WHILE Expression Invariants DO StmtList END SEMI    { WhileStmt($2,$3,$5) }
+    | CALL ID LPAREN RPAREN SEMI                          { CallStmt([],$2,[]) }
+    | CALL ID LPAREN ExprList RPAREN SEMI                 { CallStmt([],$2,$4) }
+    | CALL VarList ID LPAREN RPAREN SEMI                  { CallStmt($2,$3,[]) }
+    | CALL VarList ID LPAREN ExprList RPAREN SEMI         { CallStmt($2,$3,$5) }
+    | ASSERT Expression SEMI                              { Assert($2) }
+
+Invariants:
+                                       { [] }
+    | INVARIANT Expression Invariants  { $2::$3 }
diff --git a/Source/Forro/Printer.fs b/Source/Forro/Printer.fs
index 2a9eac84..d168e094 100644
--- a/Source/Forro/Printer.fs
+++ b/Source/Forro/Printer.fs
@@ -1,107 +1,107 @@
-module ForroPrinter

-

-open System

-open Forro

-

-let PrintField f =

-    printf "."

-    match f with

-    | Head -> printf "head"

-    | Tail -> printf "tail"

-    | Valid -> printf "valid"

-

-let PrintOp op =

-    printf " "

-    match op with

-    | Eq -> printf "=="

-    | Neq -> printf "!="

-    | Plus -> printf "+"

-    | Minus -> printf "-"

-    | Times -> printf "*"

-    | Less -> printf "<"

-    | AtMost -> printf "<="

-    | And -> printf "and"

-    | Or -> printf "or"

-    printf " "

-

-let rec PrintExpr e outermost =

-    match e with

-    | Constant(x) -> printf "%i" x

-    | Null -> printf "null"

-    | Identifier(Var(x)) -> printf "%s" x

-    | Not(e) -> printf "not(" ; PrintExpr e true ; printf ")"

-    | Binary(op,a,b) ->

-        if outermost then () else printf "("

-        PrintExpr a false ; PrintOp op ; PrintExpr b false

-        if outermost then () else printf ")"

-    | Select(e,f) -> PrintExpr e false ; PrintField f

-    | Old(e) -> printf "old(" ; PrintExpr e true ; printf ")"

-

-let rec Indent n =

-    if n = 0 then () else printf " " ; Indent (n-1)

-

-let rec PrintStmt indent s =

-    Indent indent

-    let ind = indent + 2

-    match s with

-    | Assign(Var(x), e) -> printf "%s" x ; printf " := " ; PrintExpr e true

-    | Update(obj,f,rhs) -> PrintExpr obj false ; PrintField f ; printf " := " ; PrintExpr rhs true

-    | Alloc(Var(x),hd,tl) -> printf "%s" x ; printf " := new (" ; PrintExpr hd false ; printf ", " ; PrintExpr tl false ; printf ")"

-    | IfStmt(guard,thn,els) ->

-        printf "if " ; PrintExpr guard true ; printfn " then"

-        PrintStmtList ind thn

-        Indent indent ; printfn "else"

-        PrintStmtList ind els

-        Indent indent ; printf "end"

-    | WhileStmt(guard,invs,body) ->

-        printf "while " ; PrintExpr guard true ; printfn ""

-        List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv true ; printfn "") invs

-        Indent indent ; printfn "do"

-        PrintStmtList ind body

-        Indent indent ; printf "end"

-    | CallStmt(outs,id,ins) ->

-        printf "call "

-        if outs.IsEmpty then () else

-            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="

-        printf " %s" id

-        printf "("

-        ignore (List.fold (fun sep e -> printf "%s" sep ; PrintExpr e false ; ", ") "" ins)

-        printf ")"

-    | Assert(e) ->

-        printf "assert " ; PrintExpr e true

-    printfn ";"

-

-and PrintStmtList indent slist =

-    match slist with

-    | Block(ss) -> List.iter (fun s -> PrintStmt indent s) ss

-

-let PrintProc p =

-    match p with

-    | Proc(name, ins, outs, req, ens, body) ->

-        // signature

-        printf "procedure "

-        if outs.IsEmpty then () else

-            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="

-        printf " %s(" name

-        ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" ins)

-        printfn ")"

-        // specification

-        printf "  requires "

-        PrintExpr req true

-        printfn ""

-        printf "  ensures "

-        PrintExpr ens true

-        printfn ""

-        // body

-        printfn "do"

-        PrintStmtList 2 body

-        printfn "end;"

-

-let rec PrintProcs ps =

-    match ps with

-    | [] -> ()

-    | p::rest -> PrintProc p ; PrintProcs rest

-

-let Print prog =

-    match prog with

-    | Prog(procs) -> PrintProcs procs

+module ForroPrinter
+
+open System
+open Forro
+
+let PrintField f =
+    printf "."
+    match f with
+    | Head -> printf "head"
+    | Tail -> printf "tail"
+    | Valid -> printf "valid"
+
+let PrintOp op =
+    printf " "
+    match op with
+    | Eq -> printf "=="
+    | Neq -> printf "!="
+    | Plus -> printf "+"
+    | Minus -> printf "-"
+    | Times -> printf "*"
+    | Less -> printf "<"
+    | AtMost -> printf "<="
+    | And -> printf "and"
+    | Or -> printf "or"
+    printf " "
+
+let rec PrintExpr e outermost =
+    match e with
+    | Constant(x) -> printf "%i" x
+    | Null -> printf "null"
+    | Identifier(Var(x)) -> printf "%s" x
+    | Not(e) -> printf "not(" ; PrintExpr e true ; printf ")"
+    | Binary(op,a,b) ->
+        if outermost then () else printf "("
+        PrintExpr a false ; PrintOp op ; PrintExpr b false
+        if outermost then () else printf ")"
+    | Select(e,f) -> PrintExpr e false ; PrintField f
+    | Old(e) -> printf "old(" ; PrintExpr e true ; printf ")"
+
+let rec Indent n =
+    if n = 0 then () else printf " " ; Indent (n-1)
+
+let rec PrintStmt indent s =
+    Indent indent
+    let ind = indent + 2
+    match s with
+    | Assign(Var(x), e) -> printf "%s" x ; printf " := " ; PrintExpr e true
+    | Update(obj,f,rhs) -> PrintExpr obj false ; PrintField f ; printf " := " ; PrintExpr rhs true
+    | Alloc(Var(x),hd,tl) -> printf "%s" x ; printf " := new (" ; PrintExpr hd false ; printf ", " ; PrintExpr tl false ; printf ")"
+    | IfStmt(guard,thn,els) ->
+        printf "if " ; PrintExpr guard true ; printfn " then"
+        PrintStmtList ind thn
+        Indent indent ; printfn "else"
+        PrintStmtList ind els
+        Indent indent ; printf "end"
+    | WhileStmt(guard,invs,body) ->
+        printf "while " ; PrintExpr guard true ; printfn ""
+        List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv true ; printfn "") invs
+        Indent indent ; printfn "do"
+        PrintStmtList ind body
+        Indent indent ; printf "end"
+    | CallStmt(outs,id,ins) ->
+        printf "call "
+        if outs.IsEmpty then () else
+            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
+        printf " %s" id
+        printf "("
+        ignore (List.fold (fun sep e -> printf "%s" sep ; PrintExpr e false ; ", ") "" ins)
+        printf ")"
+    | Assert(e) ->
+        printf "assert " ; PrintExpr e true
+    printfn ";"
+
+and PrintStmtList indent slist =
+    match slist with
+    | Block(ss) -> List.iter (fun s -> PrintStmt indent s) ss
+
+let PrintProc p =
+    match p with
+    | Proc(name, ins, outs, req, ens, body) ->
+        // signature
+        printf "procedure "
+        if outs.IsEmpty then () else
+            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
+        printf " %s(" name
+        ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" ins)
+        printfn ")"
+        // specification
+        printf "  requires "
+        PrintExpr req true
+        printfn ""
+        printf "  ensures "
+        PrintExpr ens true
+        printfn ""
+        // body
+        printfn "do"
+        PrintStmtList 2 body
+        printfn "end;"
+
+let rec PrintProcs ps =
+    match ps with
+    | [] -> ()
+    | p::rest -> PrintProc p ; PrintProcs rest
+
+let Print prog =
+    match prog with
+    | Prog(procs) -> PrintProcs procs
diff --git a/Source/Forro/Resolver.fs b/Source/Forro/Resolver.fs
index f227a5ca..9209f640 100644
--- a/Source/Forro/Resolver.fs
+++ b/Source/Forro/Resolver.fs
@@ -1,123 +1,123 @@
-module Resolver

-

-open System

-open Forro

-

-exception ResolutionError of string

-

-let ResolutionError(s: string) =

-    raise (ResolutionError s)

-

-type VarKind = InParam | OutParam | Local

-

-type Context(procedures: Collections.Generic.IDictionary<string,Procedure>) =

-    let mutable locals = null

-    let mutable ProcName = ""

-    member c.Procedures = procedures

-    member c.StartNewProcedure procName =

-        ProcName <- procName

-        locals <- new Collections.Generic.Dictionary<string,VarKind>()

-    member c.AddLocal v kind =

-        let name = VarName v

-        if locals.ContainsKey name then ResolutionError ("duplicate variable '" + name + "' in procedure '" + ProcName + "'") else ()

-        locals.Add(name, kind)

-    member c.HasLocal v =

-        locals.ContainsKey (VarName v)

-    member c.IncludeAssignmentTarget v =

-        let name = VarName v

-        if locals.ContainsKey name then

-            let kind = locals.Item name

-            if kind = VarKind.InParam then ResolutionError ("variable '"+ name + "' is an in-parameter, which cannot be used as an assignment target") else ()

-        else

-            locals.Add(name, VarKind.Local)

-    member v.GetLocals = locals

-

-let rec ResolveExpr (ctx: Context) expr twoState specContext =

-    match expr with

-    | Constant(x) -> ()

-    | Null -> ()

-    | Identifier(v) ->

-        if ctx.HasLocal v then () else ResolutionError ("undefined variable: " + VarName v)

-    | Not(e) -> ResolveExpr ctx e twoState specContext

-    | Binary(op,a,b) ->

-        ResolveExpr ctx a twoState specContext

-        ResolveExpr ctx b twoState specContext

-    | Select(e,f) ->

-        ResolveExpr ctx e twoState specContext

-        match f with

-        | Valid -> if specContext then () else ResolutionError "valid can only be used in specification contexts"

-        | _ -> ()

-    | Old(e) ->

-        if twoState then () else ResolutionError "old expressions can only be used in two-state contexts"

-        ResolveExpr ctx e twoState specContext

-

-let rec ResolveStmt ctx s =

-    match s with

-    | Assign(v, e) ->

-        ResolveExpr ctx e false false

-        ctx.IncludeAssignmentTarget v

-    | Update(obj,f,rhs) ->

-        ResolveExpr ctx obj false false

-        match f with

-        | Valid -> ResolutionError "valid can only be used in specification contexts (in particular, it cannot be assigned to)"

-        | _ -> ()

-        ResolveExpr ctx rhs false false

-    | Alloc(v,hd,tl) ->

-        ResolveExpr ctx hd false false

-        ResolveExpr ctx tl false false

-        ctx.IncludeAssignmentTarget v

-    | IfStmt(guard,thn,els) ->

-        ResolveExpr ctx guard false false

-        ResolveStmtList ctx thn

-        ResolveStmtList ctx els

-    | WhileStmt(guard,invs,body) ->

-        ResolveExpr ctx guard false false

-        List.iter (fun inv -> ResolveExpr ctx inv true true) invs

-        ResolveStmtList ctx body

-    | CallStmt(outs,name,ins) ->

-        if ctx.Procedures.ContainsKey name then () else ResolutionError ("call to undefined procedure: " + name)

-        match ctx.Procedures.Item name with

-        | Proc(_,fIns,fOuts,_,_,_) ->

-            if fIns.Length = ins.Length then () else ResolutionError ("call to " + name + " has wrong number of in-parameters (got " + ins.Length.ToString() + ", expected " + fIns.Length.ToString() + ")")

-            if fOuts.Length = outs.Length then () else ResolutionError ("call to " + name + " has wrong number of out-parameters (got " + outs.Length.ToString() + ", expected " + fOuts.Length.ToString() + ")")

-        List.iter (fun e -> ResolveExpr ctx e false false) ins

-        let outnames = new Collections.Generic.Dictionary<string,Variable>()

-        List.iter (fun v ->

-            ctx.IncludeAssignmentTarget v

-            let name = VarName v

-            if outnames.ContainsKey name then ResolutionError ("an actual out-parameter is allowed only once for a call: " + name) else ()

-            outnames.Add(name, v)

-            ) outs

-    | Assert(e) ->

-        ResolveExpr ctx e true true

-

-and ResolveStmtList ctx slist =

-    match slist with

-    | Block(ss) -> List.iter (fun s -> ResolveStmt ctx s) ss

-

-let ProcedureName p =

-    match p with Proc(id,_,_,_,_,_) -> id

-

-let ResolveProc (ctx: Context) p =

-    match p with

-    | Proc(name, ins, outs, req, ens, body) ->

-        // look up 'name' in ctx.Procedures, report an error if it is not 'p'

-        let q = ctx.Procedures.Item name

-        if p <> q then ResolutionError ("duplicate procedure: " + name) else ()

-        ctx.StartNewProcedure name

-        // look for duplicates in ins+outs

-        List.iter (fun v -> ctx.AddLocal v VarKind.InParam) ins

-        List.iter (fun v -> ctx.AddLocal v VarKind.OutParam) outs

-        // resolve specification

-        ResolveExpr ctx req false true

-        ResolveExpr ctx ens true true

-        // resolve body

-        ResolveStmtList ctx body

-        ctx.GetLocals

-

-let Resolve prog =

-    match prog with

-    | Prog(procs) ->

-        let procedures = dict [ for p in procs -> ProcedureName p, p ]

-        let ctx = Context(procedures)

-        List.map (fun p -> p, ResolveProc ctx p) procs

+module Resolver
+
+open System
+open Forro
+
+exception ResolutionError of string
+
+let ResolutionError(s: string) =
+    raise (ResolutionError s)
+
+type VarKind = InParam | OutParam | Local
+
+type Context(procedures: Collections.Generic.IDictionary<string,Procedure>) =
+    let mutable locals = null
+    let mutable ProcName = ""
+    member c.Procedures = procedures
+    member c.StartNewProcedure procName =
+        ProcName <- procName
+        locals <- new Collections.Generic.Dictionary<string,VarKind>()
+    member c.AddLocal v kind =
+        let name = VarName v
+        if locals.ContainsKey name then ResolutionError ("duplicate variable '" + name + "' in procedure '" + ProcName + "'") else ()
+        locals.Add(name, kind)
+    member c.HasLocal v =
+        locals.ContainsKey (VarName v)
+    member c.IncludeAssignmentTarget v =
+        let name = VarName v
+        if locals.ContainsKey name then
+            let kind = locals.Item name
+            if kind = VarKind.InParam then ResolutionError ("variable '"+ name + "' is an in-parameter, which cannot be used as an assignment target") else ()
+        else
+            locals.Add(name, VarKind.Local)
+    member v.GetLocals = locals
+
+let rec ResolveExpr (ctx: Context) expr twoState specContext =
+    match expr with
+    | Constant(x) -> ()
+    | Null -> ()
+    | Identifier(v) ->
+        if ctx.HasLocal v then () else ResolutionError ("undefined variable: " + VarName v)
+    | Not(e) -> ResolveExpr ctx e twoState specContext
+    | Binary(op,a,b) ->
+        ResolveExpr ctx a twoState specContext
+        ResolveExpr ctx b twoState specContext
+    | Select(e,f) ->
+        ResolveExpr ctx e twoState specContext
+        match f with
+        | Valid -> if specContext then () else ResolutionError "valid can only be used in specification contexts"
+        | _ -> ()
+    | Old(e) ->
+        if twoState then () else ResolutionError "old expressions can only be used in two-state contexts"
+        ResolveExpr ctx e twoState specContext
+
+let rec ResolveStmt ctx s =
+    match s with
+    | Assign(v, e) ->
+        ResolveExpr ctx e false false
+        ctx.IncludeAssignmentTarget v
+    | Update(obj,f,rhs) ->
+        ResolveExpr ctx obj false false
+        match f with
+        | Valid -> ResolutionError "valid can only be used in specification contexts (in particular, it cannot be assigned to)"
+        | _ -> ()
+        ResolveExpr ctx rhs false false
+    | Alloc(v,hd,tl) ->
+        ResolveExpr ctx hd false false
+        ResolveExpr ctx tl false false
+        ctx.IncludeAssignmentTarget v
+    | IfStmt(guard,thn,els) ->
+        ResolveExpr ctx guard false false
+        ResolveStmtList ctx thn
+        ResolveStmtList ctx els
+    | WhileStmt(guard,invs,body) ->
+        ResolveExpr ctx guard false false
+        List.iter (fun inv -> ResolveExpr ctx inv true true) invs
+        ResolveStmtList ctx body
+    | CallStmt(outs,name,ins) ->
+        if ctx.Procedures.ContainsKey name then () else ResolutionError ("call to undefined procedure: " + name)
+        match ctx.Procedures.Item name with
+        | Proc(_,fIns,fOuts,_,_,_) ->
+            if fIns.Length = ins.Length then () else ResolutionError ("call to " + name + " has wrong number of in-parameters (got " + ins.Length.ToString() + ", expected " + fIns.Length.ToString() + ")")
+            if fOuts.Length = outs.Length then () else ResolutionError ("call to " + name + " has wrong number of out-parameters (got " + outs.Length.ToString() + ", expected " + fOuts.Length.ToString() + ")")
+        List.iter (fun e -> ResolveExpr ctx e false false) ins
+        let outnames = new Collections.Generic.Dictionary<string,Variable>()
+        List.iter (fun v ->
+            ctx.IncludeAssignmentTarget v
+            let name = VarName v
+            if outnames.ContainsKey name then ResolutionError ("an actual out-parameter is allowed only once for a call: " + name) else ()
+            outnames.Add(name, v)
+            ) outs
+    | Assert(e) ->
+        ResolveExpr ctx e true true
+
+and ResolveStmtList ctx slist =
+    match slist with
+    | Block(ss) -> List.iter (fun s -> ResolveStmt ctx s) ss
+
+let ProcedureName p =
+    match p with Proc(id,_,_,_,_,_) -> id
+
+let ResolveProc (ctx: Context) p =
+    match p with
+    | Proc(name, ins, outs, req, ens, body) ->
+        // look up 'name' in ctx.Procedures, report an error if it is not 'p'
+        let q = ctx.Procedures.Item name
+        if p <> q then ResolutionError ("duplicate procedure: " + name) else ()
+        ctx.StartNewProcedure name
+        // look for duplicates in ins+outs
+        List.iter (fun v -> ctx.AddLocal v VarKind.InParam) ins
+        List.iter (fun v -> ctx.AddLocal v VarKind.OutParam) outs
+        // resolve specification
+        ResolveExpr ctx req false true
+        ResolveExpr ctx ens true true
+        // resolve body
+        ResolveStmtList ctx body
+        ctx.GetLocals
+
+let Resolve prog =
+    match prog with
+    | Prog(procs) ->
+        let procedures = dict [ for p in procs -> ProcedureName p, p ]
+        let ctx = Context(procedures)
+        List.map (fun p -> p, ResolveProc ctx p) procs
diff --git a/Source/Forro/Translator.fs b/Source/Forro/Translator.fs
index 4e7be216..db771c96 100644
--- a/Source/Forro/Translator.fs
+++ b/Source/Forro/Translator.fs
@@ -1,217 +1,217 @@
-module Translator

-

-open Forro

-open BoogieAst

-open Resolver

-open System.Collections.Generic

-

-let rec Append a b =

-    match a with

-    | [] -> b

-    | hd::tl -> hd::(Append tl b)

-

-let rec Flatten a =

-    match a with

-    | [] -> []

-    | list::rest -> Append list (Flatten rest)

-

-// ---------- Prelude ----------

-

-let Prelude =

-    @"// Forro

-

-var $head: [int]int;  // int -> int

-var $tail: [int]int;

-var $valid: [int]bool;  // array int of bool

-

-const null: int;

-

-function GoodState([int]int, [int]int, [int]bool): bool;

-

-axiom (forall hd, tl: [int]int, valid: [int]bool ::

-        { GoodState(hd, tl, valid) }

-        GoodState(hd, tl, valid) ==> !valid[null]);

-"

-

-// ---------- Translate Expressions ----------

-

-let TrField f =

-    match f with

-    | Head -> "$head"

-    | Tail -> "$tail"

-    | Valid -> "$valid"

-

-let AllFields = ["$head" ; "$tail" ; "$valid"]

-

-let MkPred term =

-    match term with

-    | BToTerm(p) -> p

-    | _ -> BToPred(term)

-

-let MkTerm pred =

-    match pred with

-    | BToPred(e) -> e

-    | _ -> BToTerm(pred)

-

-let rec TrExpr expr =

-    match expr with

-    | Constant(x) -> BConstant x

-    | Null -> BNull

-    | Identifier(Var(x)) -> BIdentifier(x)

-    | Not(e) -> BNot(TrExpr e)

-    | Binary(op,a,b) ->

-        let a = TrExpr a

-        let b = TrExpr b

-        match op with

-        | Eq -> MkTerm(BBinary(BEq,a,b))

-        | Neq -> MkTerm(BBinary(BNeq,a,b))

-        | Plus -> BBinary(BPlus,a,b)

-        | Minus -> BBinary(BMinus,a,b)

-        | Times -> BBinary(BTimes,a,b)

-        | Less -> MkTerm(BBinary(BLess,a,b))

-        | AtMost -> MkTerm(BBinary(BAtMost,a,b))

-        | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b))

-        | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b))

-    | Select(e,f) ->

-        let r = BSelect(TrField f, TrExpr e)

-        if f = Field.Valid then MkTerm(r) else r

-    | Old(e) -> BOld(TrExpr e)

-

-let rec ListToConjunction list =

-    match list with

-    | [] -> BTrue

-    | [P] -> P

-    | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl)

-

-let rec DefL expr =

-    match expr with

-    | Constant(x) -> []

-    | Null -> []

-    | Identifier(Var(x)) -> []

-    | Not(e) -> DefL e

-    | Binary(op,a,b) ->

-        match op with

-        | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a)   // (Def a) && ((TrExpr a) ==> (Def b))

-        | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a)  // (Def a) && (!(TrExpr a) ==> (Def b))

-        | _ -> Append (DefL b) (DefL a)

-    | Select(e,f) ->

-        let def = DefL e

-        if f = Field.Valid then def  // it is always okay to ask about .valid

-        else BSelect("$valid", TrExpr e) :: def

-    | Old(e) -> List.map BOld (DefL e)

-

-and Def expr =

-    ListToConjunction (List.rev (DefL expr))

-

-let AssumeGoodState =

-    BAssume (BFunc("GoodState", List.map BIdentifier AllFields))

-

-// ---------- Translate Statements ----------

-

-type LocalBookkeeping = LB of int * BVarDecl list

-

-let FreshLocal locals =

-    match locals with

-    | LB(n, vars) ->

-        let name = "nw$" + n.ToString()

-        (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars))

-

-let rec TrStmt stmt locals =

-    match stmt with

-    | Assign(v,e) ->

-        let s = [ BAssert (Def e) ;

-                  BAssign(VarName v, TrExpr e) ]

-        (s, locals)

-    | Update(obj,f,rhs) ->

-        let o = TrExpr obj

-        let s = [ BAssert(Def obj) ; BAssert (Def rhs) ;

-                  BAssert(BSelect("$valid", o)) ;

-                  BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ;

-                  AssumeGoodState ]

-        (s, locals)

-    | Alloc(v,hd,tl) ->

-        let nw, name, locals = FreshLocal locals

-        let s = [ BAssert (Def hd) ; BAssert (Def tl) ;

-                  BHavoc [name] ;

-                  BAssume(BNot(BSelect("$valid", nw))) ;

-                  BAssume(BBinary(BEq, BSelect("$head", nw), TrExpr hd)) ;

-                  BAssume(BBinary(BEq, BSelect("$tail", nw), TrExpr tl)) ;

-                  BUpdate("$valid", nw, BTrue) ;

-                  AssumeGoodState ;

-                  BAssign(VarName v, nw) ]

-        (s, locals)

-    | IfStmt(guard,thn,els) ->

-        let check = BAssert(Def guard)

-        let thn, locals = TrStmtList thn locals

-        let els, locals = TrStmtList els locals

-        let s = BIfStmt(MkPred (TrExpr guard), thn, els)

-        ([check ; s], locals)

-    | WhileStmt(guard,invs,body) ->

-        let ii = [Def guard]

-        let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs

-        let s, locals = TrStmtList body locals

-        match s with

-        | BBlock(slist) ->

-            ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist)) ; AssumeGoodState], locals)

-    | CallStmt(outs,id,ins) ->

-        let check = List.map (fun e -> BAssert (Def e)) ins

-        let ins = List.map (fun e -> TrExpr e) ins

-        let outs = List.map (fun p -> VarName p) outs

-        let s = BCallStmt(outs, id + "#Proc", ins)

-        (Append check [s ; AssumeGoodState ], locals)

-    | Assert(e) ->

-        ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals)

-

-and TrStmtList slist locals =

-    match slist with

-    | Block([]) -> (BBlock [], locals)

-    | Block(s::rest) ->

-        let s,locals = TrStmt s locals

-        let rest,locals = TrStmtList (Block rest) locals

-        match rest with

-        | BBlock(slist) -> (BBlock(Append s slist), locals)

-

-// ---------- Translate Procedure Body ----------

-

-let TrSignature ins outs =

-    let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins

-    let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs

-    (bIns, bOuts)

-

-let LocalDecls (vars: Dictionary<string,VarKind>) =

-    Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ]

-

-let TrProc proc vars =

-    match proc with

-    | Proc(id, ins, outs, req, ens, body) ->

-        let bIns, bOuts = TrSignature ins outs

-        let pre = MkPred (TrExpr req)

-        let post = MkPred (TrExpr ens)

-        let locals = LocalDecls vars

-        let b, locals = TrStmtList body (LB(0,locals))

-        match b, locals with

-        | BBlock(slist), LB(n, vars) ->

-            BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post,

-               List.rev vars, BBlock(AssumeGoodState::slist))

-

-// --------------------

-

-let TrSpec proc vars =

-    match proc with

-    | Proc(id, ins, outs, req, ens, body) ->

-        let bIns, bOuts = TrSignature ins outs

-        let b = [ AssumeGoodState ;

-                  BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ;

-                  BHavoc AllFields ; AssumeGoodState ;

-                  BAssert (Def ens) ]

-        BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b))

-

-let TrProcedure rproc =

-    match rproc with

-    | proc, (vars: Dictionary<string,VarKind>) ->

-        let name = ProcedureName proc

-        (TrSpec proc vars, TrProc proc vars)

-

-let Translate (rprog: (Procedure * Dictionary<string,VarKind>) list) =

-    let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog)

-    BProg(Prelude, procs)

+module Translator
+
+open Forro
+open BoogieAst
+open Resolver
+open System.Collections.Generic
+
+let rec Append a b =
+    match a with
+    | [] -> b
+    | hd::tl -> hd::(Append tl b)
+
+let rec Flatten a =
+    match a with
+    | [] -> []
+    | list::rest -> Append list (Flatten rest)
+
+// ---------- Prelude ----------
+
+let Prelude =
+    @"// Forro
+
+var $head: [int]int;  // int -> int
+var $tail: [int]int;
+var $valid: [int]bool;  // array int of bool
+
+const null: int;
+
+function GoodState([int]int, [int]int, [int]bool): bool;
+
+axiom (forall hd, tl: [int]int, valid: [int]bool ::
+        { GoodState(hd, tl, valid) }
+        GoodState(hd, tl, valid) ==> !valid[null]);
+"
+
+// ---------- Translate Expressions ----------
+
+let TrField f =
+    match f with
+    | Head -> "$head"
+    | Tail -> "$tail"
+    | Valid -> "$valid"
+
+let AllFields = ["$head" ; "$tail" ; "$valid"]
+
+let MkPred term =
+    match term with
+    | BToTerm(p) -> p
+    | _ -> BToPred(term)
+
+let MkTerm pred =
+    match pred with
+    | BToPred(e) -> e
+    | _ -> BToTerm(pred)
+
+let rec TrExpr expr =
+    match expr with
+    | Constant(x) -> BConstant x
+    | Null -> BNull
+    | Identifier(Var(x)) -> BIdentifier(x)
+    | Not(e) -> BNot(TrExpr e)
+    | Binary(op,a,b) ->
+        let a = TrExpr a
+        let b = TrExpr b
+        match op with
+        | Eq -> MkTerm(BBinary(BEq,a,b))
+        | Neq -> MkTerm(BBinary(BNeq,a,b))
+        | Plus -> BBinary(BPlus,a,b)
+        | Minus -> BBinary(BMinus,a,b)
+        | Times -> BBinary(BTimes,a,b)
+        | Less -> MkTerm(BBinary(BLess,a,b))
+        | AtMost -> MkTerm(BBinary(BAtMost,a,b))
+        | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b))
+        | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b))
+    | Select(e,f) ->
+        let r = BSelect(TrField f, TrExpr e)
+        if f = Field.Valid then MkTerm(r) else r
+    | Old(e) -> BOld(TrExpr e)
+
+let rec ListToConjunction list =
+    match list with
+    | [] -> BTrue
+    | [P] -> P
+    | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl)
+
+let rec DefL expr =
+    match expr with
+    | Constant(x) -> []
+    | Null -> []
+    | Identifier(Var(x)) -> []
+    | Not(e) -> DefL e
+    | Binary(op,a,b) ->
+        match op with
+        | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a)   // (Def a) && ((TrExpr a) ==> (Def b))
+        | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a)  // (Def a) && (!(TrExpr a) ==> (Def b))
+        | _ -> Append (DefL b) (DefL a)
+    | Select(e,f) ->
+        let def = DefL e
+        if f = Field.Valid then def  // it is always okay to ask about .valid
+        else BSelect("$valid", TrExpr e) :: def
+    | Old(e) -> List.map BOld (DefL e)
+
+and Def expr =
+    ListToConjunction (List.rev (DefL expr))
+
+let AssumeGoodState =
+    BAssume (BFunc("GoodState", List.map BIdentifier AllFields))
+
+// ---------- Translate Statements ----------
+
+type LocalBookkeeping = LB of int * BVarDecl list
+
+let FreshLocal locals =
+    match locals with
+    | LB(n, vars) ->
+        let name = "nw$" + n.ToString()
+        (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars))
+
+let rec TrStmt stmt locals =
+    match stmt with
+    | Assign(v,e) ->
+        let s = [ BAssert (Def e) ;
+                  BAssign(VarName v, TrExpr e) ]
+        (s, locals)
+    | Update(obj,f,rhs) ->
+        let o = TrExpr obj
+        let s = [ BAssert(Def obj) ; BAssert (Def rhs) ;
+                  BAssert(BSelect("$valid", o)) ;
+                  BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ;
+                  AssumeGoodState ]
+        (s, locals)
+    | Alloc(v,hd,tl) ->
+        let nw, name, locals = FreshLocal locals
+        let s = [ BAssert (Def hd) ; BAssert (Def tl) ;
+                  BHavoc [name] ;
+                  BAssume(BNot(BSelect("$valid", nw))) ;
+                  BAssume(BBinary(BEq, BSelect("$head", nw), TrExpr hd)) ;
+                  BAssume(BBinary(BEq, BSelect("$tail", nw), TrExpr tl)) ;
+                  BUpdate("$valid", nw, BTrue) ;
+                  AssumeGoodState ;
+                  BAssign(VarName v, nw) ]
+        (s, locals)
+    | IfStmt(guard,thn,els) ->
+        let check = BAssert(Def guard)
+        let thn, locals = TrStmtList thn locals
+        let els, locals = TrStmtList els locals
+        let s = BIfStmt(MkPred (TrExpr guard), thn, els)
+        ([check ; s], locals)
+    | WhileStmt(guard,invs,body) ->
+        let ii = [Def guard]
+        let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs
+        let s, locals = TrStmtList body locals
+        match s with
+        | BBlock(slist) ->
+            ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist)) ; AssumeGoodState], locals)
+    | CallStmt(outs,id,ins) ->
+        let check = List.map (fun e -> BAssert (Def e)) ins
+        let ins = List.map (fun e -> TrExpr e) ins
+        let outs = List.map (fun p -> VarName p) outs
+        let s = BCallStmt(outs, id + "#Proc", ins)
+        (Append check [s ; AssumeGoodState ], locals)
+    | Assert(e) ->
+        ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals)
+
+and TrStmtList slist locals =
+    match slist with
+    | Block([]) -> (BBlock [], locals)
+    | Block(s::rest) ->
+        let s,locals = TrStmt s locals
+        let rest,locals = TrStmtList (Block rest) locals
+        match rest with
+        | BBlock(slist) -> (BBlock(Append s slist), locals)
+
+// ---------- Translate Procedure Body ----------
+
+let TrSignature ins outs =
+    let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins
+    let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs
+    (bIns, bOuts)
+
+let LocalDecls (vars: Dictionary<string,VarKind>) =
+    Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ]
+
+let TrProc proc vars =
+    match proc with
+    | Proc(id, ins, outs, req, ens, body) ->
+        let bIns, bOuts = TrSignature ins outs
+        let pre = MkPred (TrExpr req)
+        let post = MkPred (TrExpr ens)
+        let locals = LocalDecls vars
+        let b, locals = TrStmtList body (LB(0,locals))
+        match b, locals with
+        | BBlock(slist), LB(n, vars) ->
+            BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post,
+               List.rev vars, BBlock(AssumeGoodState::slist))
+
+// --------------------
+
+let TrSpec proc vars =
+    match proc with
+    | Proc(id, ins, outs, req, ens, body) ->
+        let bIns, bOuts = TrSignature ins outs
+        let b = [ AssumeGoodState ;
+                  BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ;
+                  BHavoc AllFields ; AssumeGoodState ;
+                  BAssert (Def ens) ]
+        BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b))
+
+let TrProcedure rproc =
+    match rproc with
+    | proc, (vars: Dictionary<string,VarKind>) ->
+        let name = ProcedureName proc
+        (TrSpec proc vars, TrProc proc vars)
+
+let Translate (rprog: (Procedure * Dictionary<string,VarKind>) list) =
+    let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog)
+    BProg(Prelude, procs)