Jennisys: Parse and print

12 files changed, 669 insertions, 88 deletions

diff --git a/Jennisys/Jennisys/Jennisys.sln b/Jennisys/Jennisys.sln
index 5f0a0968..77ebb8e2 100644
--- a/Jennisys/Jennisys/Jennisys.sln
+++ b/Jennisys/Jennisys.sln
@@ -1,7 +1,7 @@
 

 Microsoft Visual Studio Solution File, Format Version 11.00

 # Visual Studio 2010

-Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Jennisys", "Jennisys.fsproj", "{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}"

+Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Jennisys", "Jennisys\Jennisys.fsproj", "{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}"

 EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index 746307a4..f527ba55 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -1,8 +1,44 @@
 namespace Ast

 open System

+open System.Numerics

+

+

+type Type =

+  | NamedType of string

+  | InstantiatedType of string * Type

+

+type VarDecl =

+  | Var of string * Type option

 

 type Expr =

+  | IntLiteral of BigInteger

   | IdLiteral of string

+  | Star

   | Dot of Expr * string

-  | BinExpr of string * Expr * Expr

+  | UnaryExpr of string * Expr

+  | BinaryExpr of (int * string) * Expr * Expr

+  | SelectExpr of Expr * Expr

+  | UpdateExpr of Expr * Expr * Expr

+  | SequenceExpr of Expr list

+  | SeqLength of Expr

+  | ForallExpr of VarDecl list * Expr

+

+type Stmt =

+  | Block of Stmt list

+  | Assign of Expr * Expr

+

+type Signature =

+  | Sig of VarDecl list * VarDecl list

+

+type Member =

+  | Field of VarDecl

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

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

+

+type TopLevelDecl =

+  | Class of string * string list * Member list

+  | Model of string * string list * VarDecl list * Expr list * Expr

+  | Code of string * string list

 

+type Program =

+  | Program of TopLevelDecl list

diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 6d060f3b..d266a065 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -4,60 +4,52 @@
 // This posting is provided "AS IS" with no warranties, and confers no rights.

 

 open System

+open System.IO

 open Microsoft.FSharp.Text.Lexing

 

 open Ast

 open Lexer

 open Parser

-

-/// Evaluate a factor

-let rec evalFactor factor =

-    match factor with

-    | Float x   -> x

-    | Integer x -> float x

-    | ParenEx x -> evalExpr x

-

-/// Evaluate a term

-and evalTerm term =

-    match term with

-    | Times (term, fact)  -> (evalTerm term) * (evalFactor fact)

-    | Divide (term, fact) -> (evalTerm term) / (evalFactor fact)

-    | Factor fact         -> evalFactor fact

-

-/// Evaluate an expression

-and evalExpr expr =

-    match expr with

-    | Plus (expr, term)  -> (evalExpr expr) + (evalTerm term)

-    | Minus (expr, term) -> (evalExpr expr) - (evalTerm term)

-    | Term term          -> evalTerm term

-

-/// Evaluate an equation

-and evalEquation eq =

-    match eq with

-    | Equation expr -> evalExpr expr

-

-printfn "Calculator"

-

-let rec readAndProcess() =

-    printf ":"

-    match Console.ReadLine() with

-    | "quit" -> ()

-    | expr ->

+open Printer

+

+

+let readAndProcess tracing (filename: string) =

+    try

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

+        // 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 }

         try

-            printfn "Lexing [%s]" expr

-            let lexbuff = LexBuffer<char>.FromString(expr)

-            

-            printfn "Parsing..."

-            let equation = Parser.start Lexer.tokenize lexbuff

-            

-            printfn "Evaluating Equation..."

-            let result = evalEquation equation

-            

-            printfn "Result: %s" (result.ToString())

-            

-        with ex ->

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

-

-        readAndProcess()

-

-readAndProcess()
\ No newline at end of file
+            // parse

+            let prog = Parser.start Lexer.tokenize lexbuf

+            // print the given Jennisys program

+            if tracing then

+                printfn "---------- Given Jennisys program ----------"

+                Print prog

+            else ()

+            // that's it

+            if tracing then printfn "----------" else ()

+        with

+        | ex ->

+            let pos = lexbuf.EndPos

+            printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message

+

+    with

+     | 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/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 831c56fc..372b8703 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -8,7 +8,7 @@
     <ProjectGuid>{f2ff4b3a-2fe8-474a-88df-6950f7d78908}</ProjectGuid>

     <OutputType>Exe</OutputType>

     <RootNamespace>Language</RootNamespace>

-    <AssemblyName>Language</AssemblyName>

+    <AssemblyName>Jennisys</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <Name>Language</Name>

@@ -56,6 +56,7 @@
     <FsLex Include="Lexer.fsl">

       <OtherFlags>--unicode</OtherFlags>

     </FsLex>

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

     <Compile Include="Jennisys.fs" />

   </ItemGroup>

   <ItemGroup>

@@ -66,6 +67,7 @@
     <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.

diff --git a/Jennisys/Jennisys/Lexer.fsl b/Jennisys/Jennisys/Lexer.fsl
index e3dbf766..9a1cc623 100644
--- a/Jennisys/Jennisys/Lexer.fsl
+++ b/Jennisys/Jennisys/Lexer.fsl
@@ -10,27 +10,64 @@ let lexeme lexbuf =
 

 // 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       { tokenize lexbuf }

+| whitespace  { tokenize lexbuf }

+| newline     { lexbuf.EndPos <- lexbuf.EndPos.NextLine; tokenize lexbuf }

+// TODO:  | "//"[-newline]* { tokenize lexbuf }

 // keywords

 | "class"    { CLASS }

 | "model"    { MODEL }

 | "code"     { CODE }

+| "var"          { VAR }

+| "constructor"  { CONSTRUCTOR }

+| "method"       { METHOD }

+| "frame"        { FRAME }

+| "invariant"    { INVARIANT }

+| "returns"      { RETURNS }

+| "requires"     { REQUIRES }

+| "forall"       { FORALL }

 // Operators

-| "+"			{ PLUS }

-| "-"			{ MINUS }

-| "*"			{ ASTER }

-| "/"			{ SLASH }

+| "."      { DOT }

+| "+"      { PLUS }

+| "-"      { MINUS }

+| "*"      { STAR }

+| "div"    { DIV }

+| "mod"    { MOD }

+| "&&"     { AND }

+| "||"     { OR }

+| "!"      { NOT }

+| "==>"    { IMPLIES }

+| "<==>"   { IFF }

+| "<"      { LESS }

+| "<="     { ATMOST }

+| "="      { EQ }

+| "!="     { NEQ }

+| ">="     { ATLEAST }

+| ">"      { GREATER }

+| "in"     { IN }

+| "!in"    { NOTIN }

 // Misc

-| "("			{ LPAREN }

-| ")"			{ RPAREN }

+| ":="     { GETS }

+| "("      { LPAREN }

+| ")"      { RPAREN }

+| "["      { LBRACKET }

+| "]"      { RBRACKET }

+| "{"      { LCURLY }

+| "}"      { RCURLY }

+| "|"      { VERTBAR }

+| ":"      { COLON }

+| "::"     { COLONCOLON }

+| ","      { COMMA }

 // Numberic constants

-| ['-']?digit+									{ INT32 (Int32.Parse(lexeme lexbuf)) }

-| ['-']?digit+('.'digit+)?(['e''E']digit+)?		{ FLOAT (Double.Parse(lexeme lexbuf)) }

+| digit+        { INTEGER (System.Numerics.BigInteger.Parse(lexeme lexbuf)) }

+// identifiers

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

 // EOF

 | eof   { EOF }

+| _ { printfn "Unrecognized input character: %s" (lexeme lexbuf) ; EOF }

 

diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy
index 279430fe..34d04d76 100644
--- a/Jennisys/Jennisys/Parser.fsy
+++ b/Jennisys/Jennisys/Parser.fsy
@@ -9,37 +9,141 @@ open Ast
 

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

 // the data carried by each token:

-%token <System.Int32> INT32

-%token <System.Double> FLOAT

-%token PLUS MINUS ASTER	SLASH

-%token LPAREN RPAREN

+%token <string> ID

+%token <System.Numerics.BigInteger> INTEGER

+%token DOT

+%token NOT

+%token STAR DIV MOD

+%token PLUS MINUS

+%token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN

+%token AND OR

+%token IMPLIES

+%token IFF

+%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 EOF

 

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

 // symbol:

-%type < Ast.Equation > start

+%type < Ast.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 { Equation($1) }

-

-Prog:

-    | Expr EOF					{ $1 }

-

-Expr: 

-    | Expr PLUS  Term			{ Plus($1, $3)  }

-    | Expr MINUS Term			{ Minus($1, $3) }

-    | Term						{ Term($1)      }

-

-Term:

-    | Term ASTER Factor			{ Times($1, $3)  }

-    | Term SLASH Factor			{ Divide($1, $3) }

-    | Factor					{ Factor($1)     }

-    

-Factor:

-    | FLOAT						{ Float($1)  }

-    | INT32						{ Integer($1) }

-    | LPAREN Expr RPAREN		{ ParenEx($2) }

+start: TopLevelDecls EOF     { Program($1) }

+

+TopLevelDecls:

+    |                             { [] }

+    | TopLevelDecl TopLevelDecls  { $1 :: $2 }

+

+TopLevelDecl:

+    | CLASS ID TypeParams LCURLY Members RCURLY                       { Class($2, $3, $5) }

+    | MODEL ID TypeParams LCURLY ConcreteVars Frame Invariant RCURLY  { Model($2, $3, $5, $6, $7) }

+    | CODE ID TypeParams LCURLY RCURLY                                { Code($2, $3) }

+

+TypeParams:

+    |                          { [] }

+    | LBRACKET IdList RBRACKET { $2 }

+

+IdList:

+    | ID            { [$1] }

+    | ID IdList     { $1 :: $2 }

+

+Members:

+    |                      { [] }

+    | Member Members       { $1 :: $2 }

+

+Signature:

+    | LPAREN VarDeclList RPAREN  { Sig($2, []) }

+    | LPAREN VarDeclList RPAREN RETURNS LPAREN VarDeclList RPAREN  { Sig($2, $6) }

+

+Pre:

+    |                           { IdLiteral "true" }

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

+

+StmtList:

+    |                    { [] }

+    | Stmt StmtList      { $1 :: $2 }

+

+Stmt:

+    | BlockStmt          { $1 }

+    | Expr GETS Expr     { Assign($1, $3) }

+

+BlockStmt:

+    | LCURLY StmtList RCURLY   { Block $2 }

+

+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) }

+

+ConcreteVars:

+    |                          { [] }

+    | VAR VarDecl ConcreteVars { $2 :: $3 }

+

+Frame:

+    |                    { [] }

+    | FRAME ExprList     { $2 }

+

+Invariant:

+    |                    { IdLiteral "true" }

+    | INVARIANT ExprList { List.fold (fun x y -> BinaryExpr((30,"&&"),x,y)) (IdLiteral "true") $2 }

+

+VarDeclList:

+    |                           { [] }

+    | VarDecl                   { [$1] }

+    | VarDecl COMMA VarDeclList { $1 :: $3 }

+

+VarDecl:

+    | ID               { Var($1,None) }

+    | ID COLON Type    { Var($1,Some($3)) }

+

+Type:

+    | ID                         { NamedType($1) }

+    | ID LBRACKET Type RBRACKET  { InstantiatedType($1, $3) }

+

+ExprList:

+    |                   { [] }

+    | Expr              { [$1] }

+    | Expr ExprList     { $1 :: $2 }

+

+Expr:

+  | INTEGER            { IntLiteral($1) }

+  | ID                 { IdLiteral($1) }

+  | STAR               { Star }

+  | Expr DOT ID        { Dot($1, $3) }

+  | UnaryOp Expr       { UnaryExpr($1, $2) }

+  | Expr BinaryOp Expr { BinaryExpr($2, $1, $3) }

+  | Expr LBRACKET Expr RBRACKET           { SelectExpr($1, $3) }

+  | Expr LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }

+  | LPAREN Expr RPAREN { $2 }

+  | LBRACKET ExprList RBRACKET            { SequenceExpr($2) }

+  | VERTBAR Expr VERTBAR                  { SeqLength($2) }

+  | FORALL VarDeclList COLONCOLON Expr    { ForallExpr($2, $4) }

+

+UnaryOp:  // unary operators have strength 90

+  | NOT      { "!" }

+  | MINUS    { "-" }

+

+BinaryOp:

+  | STAR     { 60, "*" }

+  | DIV      { 60, "div" }

+  | MOD      { 60, "mod" }

+  | PLUS     { 50, "+" }

+  | MINUS    { 50, "-" }

+  | EQ       { 40, "=" }

+  | NEQ      { 40, "!=" }

+  | LESS     { 40, "<" }

+  | ATMOST   { 40, "<=" }

+  | ATLEAST  { 40, ">=" }

+  | GREATER  { 40, ">" }

+  | IN       { 40, "in" }

+  | NOTIN    { 40, "!in" }

+  | AND      { 30, "&&" }  // Note, this one also occurs above

+  | OR       { 30, "||" }

+  | IMPLIES  { 20, "==>" }

+  | IFF      { 10, "<==>" }

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
new file mode 100644
index 00000000..da481176
--- /dev/null
+++ b/Jennisys/Jennisys/Printer.fs
@@ -0,0 +1,113 @@
+module Printer

+

+open Ast

+

+let rec PrintSep sep f list =

+  match list with

+  | [] -> ()

+  | [a] -> f a

+  | a :: more -> f a ; printf "%s" sep ; PrintSep sep f more

+  

+let rec PrintType ty =

+  match ty with

+  | NamedType(id) -> printf "%s" id

+  | InstantiatedType(id,arg) -> printf "%s[" id ; PrintType arg ; printf "]"

+

+let PrintVarDecl vd =

+  match vd with

+  | Var(id,None) -> printf "%s" id

+  | Var(id,Some(ty)) -> printf "%s: " id ; PrintType ty

+

+let rec PrintExpr ctx expr =

+  match expr with

+  | IntLiteral(n) -> printf "%O" n

+  | IdLiteral(id) -> printf "%s" id

+  | Star -> printf "*"

+  | Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id

+  | UnaryExpr(op,e) -> printf "%s" op ; PrintExpr 90 e

+  | BinaryExpr((strength,op),e0,e1) ->

+      let needParens = strength <= ctx

+      if needParens then printf "(" else ()

+      PrintExpr strength e0 ; printf " %s " op ; PrintExpr strength e1

+      if needParens then printf ")" else ()

+  | SelectExpr(e,i) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf "]"

+  | UpdateExpr(e,i,v) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf " := " ; PrintExpr 0 v ; printf "]"

+  | SequenceExpr(ee) -> printf "[" ; ee |> PrintSep ", " (PrintExpr 0) ; printf "]"

+  | SeqLength(e) -> printf "|" ; PrintExpr 0 e ; printf "|"

+  | ForallExpr(vv,e) ->

+      let needParens = ctx <> 0

+      if needParens then printf "(" else ()

+      printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e

+      if needParens then printf ")" else ()

+

+let PrintSig signature =

+  match signature with

+  | Sig(ins, outs) ->

+      printf "("

+      ins |> PrintSep ", " PrintVarDecl

+      printf ")"

+      if outs <> [] then

+        printf " returns ("

+        outs |> PrintSep ", " PrintVarDecl

+        printf ")"

+      else ()

+

+let rec ForeachConjunct f expr =

+  match expr with

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

+  | BinaryExpr((_,"&&"),e0,e1) -> ForeachConjunct f e0 ; ForeachConjunct f e1

+  | _ -> f expr

+

+let rec Indent i =

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

+

+let rec PrintStmt stmt indent =

+  match stmt with

+  | Block(stmts) ->

+      Indent indent ; printfn "{"

+      PrintStmtList stmts (indent + 2)

+      Indent indent ; printfn "}"

+  | Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ""

+and PrintStmtList stmts indent =

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

+

+let PrintRoutine signature pre body =

+  PrintSig signature

+  printfn ""

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

+  PrintStmtList body 2

+

+let PrintMember m =

+  match m with

+  | Field(vd) -> printf "  var " ; PrintVarDecl vd ; printfn ""

+  | Constructor(id,signature,pre,body) -> printf "  constructor %s" id ; PrintRoutine signature pre body

+  | Method(id,signature,pre,body) -> printf "  method %s" id ; PrintRoutine signature pre body

+      

+let PrintTopLevelDeclHeader kind id typeParams =

+  printf "%s %s" kind id

+  match typeParams with

+    | [] -> ()

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

+  printfn " {"

+

+let PrintDecl d =

+  match d with

+  | Class(id,typeParams,members) ->

+      PrintTopLevelDeclHeader "class" id typeParams

+      List.iter PrintMember members

+      printfn "}"

+  | Model(id,typeParams,vars,frame,inv) ->

+      PrintTopLevelDeclHeader "model" id typeParams

+      vars |> List.iter (fun vd -> printf "  var " ; PrintVarDecl vd ; printfn "")

+      printfn "  frame"

+      frame |> List.iter (fun fr -> printf "    " ; PrintExpr 0 fr ; printfn "")

+      printfn "  invariant"

+      inv |> ForeachConjunct (fun e -> printf "    " ; PrintExpr 0 e ; printfn "")

+      printfn "}"

+  | Code(id,typeParams) ->

+      PrintTopLevelDeclHeader "code" id typeParams

+      printfn "}"

+

+let Print prog =

+  match prog with

+  | Program(decls) -> List.iter PrintDecl decls

diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer
new file mode 100644
index 00000000..64099079
--- /dev/null
+++ b/Test/jennisys0/Answer
@@ -0,0 +1,93 @@
+

+-------------------- Prog0.jen --------------------

+Jennisys, Copyright (c) 2011, Microsoft.

+---------- Given Jennisys program ----------

+class C {

+  var a: seq[int]

+  var x: int

+  constructor Init()

+  {

+  }

+  method Update(d)

+  {

+    x := x + 1

+    {

+      nested := statement

+      yes := sirrie

+    }

+    x.f := (12 + true)[8000 := 0 <= n]

+  }

+  method Query() returns (r)

+    requires r

+    requires *

+    requires r.r.s

+    requires a[i]

+    requires a[i := 58]

+    requires hello

+    requires (hello + goodbye) - soonyousoon

+    requires 0 <= r

+  {

+  }

+  method ManyParams(x: bool, y) returns (r, s: set[MyClass], t)

+  {

+  }

+}

+model C {

+  var x: int

+  frame

+    xyz

+  invariant

+    x <= x

+}

+code C {

+}

+----------

+

+-------------------- ExtensibleArray.jen --------------------

+Jennisys, Copyright (c) 2011, Microsoft.

+---------- Given Jennisys program ----------

+class ExtensibleArray[T] {

+  var Contents: seq[T]

+  constructor Init()

+  {

+    Contents := []

+  }

+  method Get(i) returns (t)

+    requires 0 <= (i && (i < |Contents|))

+  {

+    t := Contents[i]

+  }

+  method Set(i, t)

+    requires 0 <= (i && (i < |Contents|))

+  {

+    Contents := Contents[i := t]

+  }

+  method Append(t)

+  {

+    Contents := Contents + [t]

+  }

+}

+model ExtensibleArray[T] {

+  var elements: array[T]

+  var more: ExtensibleArray[array[T]]

+  var length: int

+  var M: int

+  frame

+    elements

+    *

+    more

+    *

+    more.Contents[*]

+  invariant

+    elements != null

+    elements.Length = 256

+    (more = null) ==> (M = 0)

+    (more != null) ==> ((|more.Contents| != 0) && (M = (256 * |more.Contents|)))

+    0 <= length

+    length <= (M + 256)

+    (more != null) ==> (M < length)

+    length = |Contents|

+    (forall i :: ((0 <= i) && (i < M)) ==> (Contents[i] = more.Contents[i div 256][i mod 256]))

+    (forall i :: ((M <= i) && (i < length)) ==> (Contents[i] = elements[i - M]))

+}

+----------

diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen
new file mode 100644
index 00000000..8a6b7a6d
--- /dev/null
+++ b/Test/jennisys0/ExtensibleArray.jen
@@ -0,0 +1,47 @@
+class ExtensibleArray[T] {

+  var Contents: seq[T]

+

+  constructor Init()

+  {

+    Contents := []

+  }

+

+  method Get(i) returns (t)

+    requires (0 <= i) && i < |Contents|

+  {

+    t := Contents[i]

+  }

+

+  method Set(i, t)

+    requires (0 <= i) && i < |Contents|

+  {

+    Contents := Contents[i := t]

+  }

+

+  method Append(t)

+  {

+    Contents := Contents + [t]

+  }

+}

+

+model ExtensibleArray[T] {

+  var elements: array[T]

+  var more: ExtensibleArray[array[T]]

+  var length: int

+  var M: int

+

+  frame

+    elements * more * more.Contents[*]

+

+  invariant

+    elements != null

+    elements.Length = 256

+    ((more = null) ==> M = 0)

+    ((more != null) ==> (|more.Contents| != 0) && M = 256 * |more.Contents|)

+    (0 <= length) && (length <= M + 256)

+    ((more != null) ==> M < length)

+

+    length = |Contents|

+    (forall i :: ((0 <= i) && (i < M)) ==> Contents[i] = more.Contents[i div 256][i mod 256])

+    (forall i :: ((M <= i) && (i < length)) ==> Contents[i] = elements[i - M])

+}

diff --git a/Test/jennisys0/Prog0.jen b/Test/jennisys0/Prog0.jen
new file mode 100644
index 00000000..cd847846
--- /dev/null
+++ b/Test/jennisys0/Prog0.jen
@@ -0,0 +1,34 @@
+class C {

+  var a: seq[int]

+  var x: int

+  constructor Init()

+  { }

+  method Update(d)

+  {

+    x := x + 1

+    { nested := statement yes := sirrie }

+    x.f := (12 + true)[8000 := 0 <= n]

+  }

+  method Query() returns (r)

+    requires r

+    requires true

+    requires *

+    requires r.r.s

+    requires a[i]

+    requires a[i := 58]

+    requires (((hello)))

+    requires (((hello) + (goodbye)) - soonyousoon)

+    requires 0 <= r

+  { }

+  method ManyParams(x:bool,y) returns (r,s:set[MyClass],t)

+  { }

+}

+

+model C {

+  var x: int

+  frame xyz

+  invariant x <= x

+}

+

+code C {

+}

diff --git a/Test/jennisys0/runtest.bat b/Test/jennisys0/runtest.bat
new file mode 100644
index 00000000..419c8891
--- /dev/null
+++ b/Test/jennisys0/runtest.bat
@@ -0,0 +1,10 @@
+@echo off

+setlocal

+

+set JENNISYS_EXE=..\..\Jennisys\Jennisys\bin\Debug\Jennisys.exe

+

+for %%f in (Prog0.jen ExtensibleArray.jen) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %JENNISYS_EXE% %* /trace %%f

+)

diff --git a/Util/Emacs/jennisys-mode.el b/Util/Emacs/jennisys-mode.el
new file mode 100644
index 00000000..89bb2767
--- /dev/null
+++ b/Util/Emacs/jennisys-mode.el
@@ -0,0 +1,113 @@
+;; jennisys-mode.el - GNU Emacs mode for Jennisys

+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

+

+(defvar jennisys-mode-hook nil)

+

+(defvar jennisys-mode-map nil

+  "Keymap for Jennisys major mode")

+

+(if jennisys-mode-map nil

+  (setq jennisys-mode-map (make-keymap))

+  (define-key jennisys-mode-map "\C-c\C-c" 'jennisys-run-boogie)

+  (define-key jennisys-mode-map [(control return)] 'font-lock-fontify-buffer))

+

+(setq auto-mode-alist

+      (append

+       '(("\\.jen" . jennisys-mode))

+       auto-mode-alist))

+

+;; font-lock

+

+(defun jennisys-regexp-opt (l)

+  (concat "\\<" (concat (regexp-opt l t) "\\>")))

+

+(defconst jennisys-font-lock-keywords-1

+  (list

+   ; comments have the form /* ... */

+   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

+   ; or // ...

+   '("//\\([^

+]\\)*" . font-lock-comment-face)

+

+   `(,(jennisys-regexp-opt '(

+        "class" "model" "code"

+        "var" "constructor" "method"

+        "frame" "invariant" "returns" "requires"

+        )) . font-lock-builtin-face)

+   `(,(jennisys-regexp-opt '(

+        "if" "then" "else"

+        "forall" "exists"

+        "this" "in"

+        "false" "true" "null")) . font-lock-keyword-face)

+   `(,(jennisys-regexp-opt '("array" "bool" "int" "set" "seq")) . font-lock-type-face)

+   )

+  "Minimal highlighting for Jennisys mode")

+

+(defvar jennisys-font-lock-keywords jennisys-font-lock-keywords-1

+  "Default highlighting for Jennisys mode")

+

+;; syntax

+

+(defvar jennisys-mode-syntax-table nil

+  "Syntax table for jennisys-mode")

+

+(defun jennisys-create-syntax-table ()

+  (if jennisys-mode-syntax-table

+      ()

+    (setq jennisys-mode-syntax-table (make-syntax-table))

+    (set-syntax-table jennisys-mode-syntax-table)

+    (modify-syntax-entry ?' "w" jennisys-mode-syntax-table)

+    (modify-syntax-entry ?_ "w" jennisys-mode-syntax-table)))

+

+;; menu

+

+(require 'easymenu)

+

+(defun jennisys-menu ()

+  (easy-menu-define

+   jennisys-mode-menu (list jennisys-mode-map)

+   "Jennisys Mode Menu." 

+   '("Jennisys"

+     ["Run Boogie" jennisys-run-boogie t]

+     "---"

+     ["Recolor buffer" font-lock-fontify-buffer t]

+     "---"

+     ))

+  (easy-menu-add jennisys-mode-menu))

+

+;; commands

+

+(defun jennisys-command-line (file)

+  (concat "boogie " file))

+

+(defun jennisys-run-boogie ()

+  "run Boogie to check the Jennisys program"

+  (interactive)

+  (let ((f (buffer-name)))

+    (compile (jennisys-command-line f))))

+

+;; setting the mode

+

+(defun jennisys-mode ()

+  "Major mode for editing Jennisys programs.

+

+\\{jennisys-mode-map}"

+  (interactive)

+  (kill-all-local-variables)

+  (jennisys-create-syntax-table)

+  ; hilight

+  (make-local-variable 'font-lock-defaults)

+  (setq font-lock-defaults '(jennisys-font-lock-keywords))

+  ; indentation

+  ; (make-local-variable 'indent-line-function)

+  ; (setq indent-line-function 'jennisys-indent-line)

+  ; menu

+  ; providing the mode

+  (setq major-mode 'jennisys-mode)

+  (setq mode-name "Jennisys")

+  (use-local-map jennisys-mode-map)

+  (font-lock-mode 1)

+  (jennisys-menu)

+  (run-hooks 'jennisys-mode-hook))

+

+(provide 'jennisys-mode)