- changed the grammar to allow for arbitrary post-condition expressions

   in public classes
 - added some utility AST constructor methods for AND, OR, and some other AST
   types
 - played with generating the Valid() function
 - added a List example with Jennisys

10 files changed, 170 insertions, 26 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 5e66f5f2..d0597d5a 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -1,7 +1,9 @@
 module Analyzer

 

 open Ast

+open AstUtils

 open Printer

+open TypeChecker

 

 let rec PrintType ty =

   match ty with

@@ -73,29 +75,81 @@ let rec PrintStmt stmt indent =
 and PrintStmtList stmts indent =

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

 

-let GenerateCode methodName signature pre stmts inv assumeInvInitially =

+let GenerateCode methodName signature pre post inv assumeInvInitially =

   printfn "  method %s()" methodName

   printfn "    modifies this;"

   printfn "  {"

   if assumeInvInitially then

     // assume invariant

-    printf "    assume " ; PrintExpr 0 inv ; printfn ";"

+    printfn "    assume Valid();"

   else ()

   // print signature as local variables

   match signature with

     | Sig(ins,outs) ->

         List.concat [ins; outs] |> List.iter (fun vd -> printf "    var " ; PrintVarDecl vd ; printfn ";")

   // assume preconditions

+  printfn "    // assume precondition"

   printf "    assume " ; PrintExpr 0 pre ; printfn ";"

-  // do statements

-  stmts |> List.iter (fun s -> PrintStmt s 4)

-  // assume invariant

-  printf "    assume " ; PrintExpr 0 inv ; printfn ";"

+  // assume invariant and postcondition

+  printfn "    // assume invariant and postcondition"

+  printfn "    assume Valid();"

+  printf "    assume " ; PrintExpr 0 post ; printfn ";"

   // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible

+  printfn "    // assert false to search for a model satisfying the assumed constraints"

   printfn "    assert false;"

-  printfn "}"

+  printfn "  }"

 

-let AnalyzeComponent c =

+let GetFieldValidExpr name = 

+  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))

+

+let GetFieldsForValidExpr (allFields: VarDecl list) prog =

+  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true

+                                     | _                                   -> false)

+

+let GenFieldsValidExprList (allFields: VarDecl list) prog =

+  let fields = GetFieldsForValidExpr allFields prog

+  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)

+

+let AnalyzeComponent (prog: Program) c =

+  match c with

+  | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->

+      let aVars = Fields members

+      let allVars = List.concat [aVars ; cVars];

+      // Now print it as a Dafny program

+      printf "class %s" name

+      match typeParams with

+        | [] -> ()

+        | _ -> printf "<" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf ">"

+      printfn " {"

+      // the fields: original abstract fields plus two more copies thereof, plus and concrete fields

+      allVars |> List.iter (function Var(nm,None) -> printfn "  var %s;" nm | Var(nm,Some(tp)) -> printf "  var %s: " nm ; PrintType tp ; printfn ";")

+      printfn ""

+      // generate the Valid function

+      let invMembers = members |> List.filter (function Invariant(_) -> true | _ -> false)

+      let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat

+      let allInvs = inv :: clsInvs

+      let fieldsValid = GenFieldsValidExprList allVars prog

+      printfn "  function Valid(): bool"

+      printfn "    reads *;"

+      printfn "  {"

+      let dummy = List.concat [fieldsValid ; allInvs] |> List.fold (fun acc (e: Expr) -> 

+                                                                      if acc = "" then

+                                                                        printf "    " ; PrintExpr 0 e ; "nonempty"

+                                                                      else

+                                                                        printfn " &&" ; printf "    " ; PrintExpr 0 e; "nonempty") ""

+      printfn ""

+      printfn "  }"; printfn ""

+

+      // generate constructors and methods

+      members |> List.iter (function

+        | Constructor(methodName,signature,pre,post) -> GenerateCode methodName signature pre post inv false ; printfn ""

+        | Method(methodName,signature,pre,post)      -> GenerateCode methodName signature pre post inv true  ; printfn ""

+        | _ -> ())

+      // the end of the class

+      printfn "}" ; printfn ""

+  | _ -> assert false  // unexpected case

+

+let AnalyzeComponent_rustan c =

   match c with

   | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->

       let aVars = Fields members

@@ -131,4 +185,4 @@ let AnalyzeComponent c =
 let Analyze prog =

   match prog with

   | Program(components) ->

-      components |> List.iter AnalyzeComponent

+      components |> List.iter (AnalyzeComponent prog)

diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index fa2db0d9..b6e04d3f 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -1,4 +1,5 @@
 namespace Ast

+

 open System

 open System.Numerics

 

@@ -32,8 +33,9 @@ type Signature =
 

 type Member =

   | Field of VarDecl

-  | Constructor of string * Signature * Expr * Stmt list

-  | Method of string * Signature * Expr * Stmt list

+  | Constructor of string * Signature * Expr * Expr

+  | Method of string * Signature * Expr * Expr

+  | Invariant of Expr list

 

 type TopLevelDecl =

   | Class of string * string list * Member list

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
new file mode 100644
index 00000000..83104f5d
--- /dev/null
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -0,0 +1,26 @@
+module AstUtils

+

+open Ast

+

+let BinaryAnd (lhs: Expr) (rhs: Expr) = 

+    match lhs, rhs with

+    | IdLiteral("true"), _  -> rhs

+    | IdLiteral("false"), _ -> IdLiteral("false")

+    | _, IdLiteral("true")  -> lhs

+    | _, IdLiteral("false") -> IdLiteral("false")

+    | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

+

+let BinaryOr (lhs: Expr) (rhs: Expr) = 

+    match lhs, rhs with

+    | IdLiteral("true"), _  -> IdLiteral("true")

+    | IdLiteral("false"), _ -> rhs

+    | _, IdLiteral("true")  -> IdLiteral("true")

+    | _, IdLiteral("false") -> lhs

+    | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

+

+let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

+

+let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)

+

+let TrueLiteral = IdLiteral("true")

+let FalseLiteral = IdLiteral("false")
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index b248cf67..34e3b611 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -2,6 +2,7 @@
 // Learn more about F# at http://fsharp.net

 // Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio

 // This posting is provided "AS IS" with no warranties, and confers no rights.

+module Main

 

 open System

 open System.IO

@@ -14,7 +15,6 @@ open Printer
 open TypeChecker

 open Analyzer

 

-

 let readAndProcess tracing analyzing (filename: string) =

     try

         printfn "// Jennisys, Copyright (c) 2011, Microsoft."

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 09e829eb..159ed923 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,6 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

+    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List.jen</StartArguments>

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

@@ -42,6 +43,7 @@
   </PropertyGroup>

   <ItemGroup>

     <Compile Include="Ast.fs" />

+    <Compile Include="AstUtils.fs" />

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

       <Visible>false</Visible>

       <Link>Parser.fs</Link>

diff --git a/Jennisys/Jennisys/Lexer.fsl b/Jennisys/Jennisys/Lexer.fsl
index 9a1cc623..26195484 100644
--- a/Jennisys/Jennisys/Lexer.fsl
+++ b/Jennisys/Jennisys/Lexer.fsl
@@ -30,6 +30,7 @@ rule tokenize = parse
 | "invariant"    { INVARIANT }

 | "returns"      { RETURNS }

 | "requires"     { REQUIRES }

+| "ensures"      { ENSURES }

 | "forall"       { FORALL }

 // Operators

 | "."      { DOT }

diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy
index e9a0b2c4..0b5c2fc8 100644
--- a/Jennisys/Jennisys/Parser.fsy
+++ b/Jennisys/Jennisys/Parser.fsy
@@ -1,11 +1,12 @@
 %{

 

 open Ast

+open AstUtils

 

 let rec MyFold ee acc =

   match ee with

     | [] -> acc

-    | x::rest -> BinaryExpr(30,"&&",x, MyFold rest acc)

+    | x::rest -> BinaryAnd x (MyFold rest acc)

 

 %}

 

@@ -27,7 +28,7 @@ let rec MyFold ee acc =
 %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR

 %token GETS COLON COLONCOLON COMMA

 %token CLASS MODEL CODE

-%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES FORALL

+%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL

 %token EOF

 

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

@@ -68,7 +69,11 @@ Signature:
 

 Pre:

     |                           { IdLiteral "true" }

-    | REQUIRES Expr Pre         { BinaryExpr(30,"&&", $2, $3) }

+    | REQUIRES Expr Pre         { BinaryAnd $2 $3 }

+

+Post: 

+    |                           { IdLiteral "true" }

+	| ENSURES Expr Post         { BinaryAnd $2 $3 }

 

 StmtList:

     |                    { [] }

@@ -83,8 +88,9 @@ BlockStmt:
 

 Member:

     | VAR VarDecl                            { Field($2) }

-    | CONSTRUCTOR ID Signature Pre StmtList  { Constructor($2, $3, $4, $5) }

-    | METHOD ID Signature Pre StmtList       { Method($2, $3, $4, $5) }

+    | CONSTRUCTOR ID Signature Pre Post      { Constructor($2, $3, $4, $5) }

+	| METHOD ID Signature Pre Post           { Method($2, $3, $4, $5) }

+	| INVARIANT ExprList                     { Invariant($2) }

 

 FrameMembers:

     |                                        { [], [], IdLiteral("true") }

@@ -128,14 +134,14 @@ Expr20:
 

 Expr30:

     | Expr40               { $1 }

-    | Expr40 AND Expr30and { BinaryExpr(30,"&&",$1,$3) }

-    | Expr40 OR Expr30or   { BinaryExpr(30,"||",$1,$3) }

+    | Expr40 AND Expr30and { BinaryAnd $1 $3 }

+    | Expr40 OR Expr30or   { BinaryOr  $1 $3 }

 Expr30and:

     | Expr40               { $1 }

-    | Expr40 AND Expr30and { BinaryExpr(30,"&&",$1,$3) }

+    | Expr40 AND Expr30and { BinaryAnd $1 $3 }

 Expr30or:

     | Expr40               { $1 }

-    | Expr40 AND Expr30or  { BinaryExpr(30,"||",$1,$3) }

+    | Expr40 AND Expr30or  { BinaryOr $1 $3 }

 

 Expr40:

     | Expr50                { $1 }

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 21193c96..f8434de5 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -75,7 +75,7 @@ let PrintRoutine signature pre body =
   PrintSig signature

   printfn ""

   pre |> ForeachConjunct (fun e -> printf "    requires " ; PrintExpr 0 e ; printfn "")

-  PrintStmtList body 4

+  PrintExpr 0 body  //  PrintStmtList body 4

 

 let PrintMember m =

   match m with

diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs
index c9e5f308..41ffbb5d 100644
--- a/Jennisys/Jennisys/TypeChecker.fs
+++ b/Jennisys/Jennisys/TypeChecker.fs
@@ -4,23 +4,34 @@ open Ast
 open System.Collections.Generic

 

 let GetClass name decls =

-  match decls |> List.tryFind (function Class(_,_,_) -> true | _ -> false) with

+  match decls |> List.tryFind (function Class(n,_,_) when n = name -> true | _ -> false) with

     | Some(cl) -> cl

     | None -> Class(name,[],[])

 

 let GetModel name decls =

-  match decls |> List.tryFind (function Model(_,_,_,_,_) -> true | _ -> false) with

+  match decls |> List.tryFind (function Model(n,_,_,_,_) when n = name -> true | _ -> false) with

     | Some(m) -> m

     | None -> Model(name,[],[],[],IdLiteral("true"))

 

 let GetCode name decls =

-  match decls |> List.tryFind (function Code(_,_) -> true | _ -> false) with

+  match decls |> List.tryFind (function Code(n,_) when n = name -> true | _ -> false) with

     | Some(c) -> c

     | None -> Code(name,[])

 

+let IsUserType prog tpo =

+  match tpo with

+    | Some(tp) ->

+        let tpname = match tp with

+                       | NamedType(tname) -> tname

+                       | InstantiatedType(tname, _) -> tname

+        match prog with

+         | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true

+                                                                      | _                                               -> false) |> List.isEmpty |> not

+    | None -> false

+

 let TypeCheck prog =

   match prog with

-  | SProgram(decls) ->

+    | SProgram(decls) ->

       let componentNames = decls |> List.choose (function Class(name,_,_) -> Some(name) | _ -> None)

       let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))

       Some(Program(clist))

diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
new file mode 100644
index 00000000..89716f8b
--- /dev/null
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -0,0 +1,42 @@
+class List[T] {
+  var list: seq[T]
+
+  constructor Init() 
+    ensures list = []
+
+  constructor Singleton(t)
+    ensures list = [t]
+}
+
+model List[T] {
+  var root: Node[T]
+
+  frame
+    root * root.list[*]
+
+  invariant
+    (root = null) ==> (|list| = 0)
+    root != null ==> list = root.list
+}
+
+class Node[T] {
+  var list: seq[T]
+
+  invariant
+    |list| > 0
+
+  constructor Init(t)
+    ensures list = [t]
+}
+
+model Node[T] {
+  var data: T
+  var next: Node[T]
+
+  frame 
+    data * next
+
+  invariant
+    next = null ==> list = [data]
+    next != null ==> list = [data] + next.list
+}