diff options
| -rw-r--r-- | Jennisys/Jennisys/Parser.fsy | 20 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Printer.fs | 2 | ||||
| -rw-r--r-- | Test/jennisys0/Answer | 20 | ||||
| -rw-r--r-- | Test/jennisys0/ExtensibleArray.jen | 8 | ||||
| -rw-r--r-- | Test/jennisys0/Prog0.jen | 11 |
5 files changed, 24 insertions, 37 deletions
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index b4b663e1..d8ffd454 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -86,8 +86,13 @@ ConcreteVars: | VAR VarDecl ConcreteVars { $2 :: $3 }
Frame:
- | { [] }
- | FRAME ExprList { $2 }
+ | { [] }
+ | FRAME { [] }
+ | FRAME FramePartitionList { $2 }
+
+FramePartitionList:
+ | FramePartition { $1 }
+ | FramePartition FramePartitionList { List.append $1 $2 }
Invariant:
| { IdLiteral "true" }
@@ -163,11 +168,18 @@ Expr90: Expr100:
| INTEGER { IntLiteral($1) }
| ID { IdLiteral($1) }
- | STAR { Star }
| Expr100 DOT ID { Dot($1, $3) }
- | Expr100 LBRACKET Expr RBRACKET { SelectExpr($1, $3) }
+ | Expr100 LBRACKET StarExpr RBRACKET { SelectExpr($1, $3) }
| Expr100 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) }
+
+StarExpr:
+ | STAR { Star }
+ | Expr { $1 }
+
+FramePartition:
+ | Expr100 { [$1] }
+ | Expr100 STAR FramePartition { $1 :: $3 }
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index d92817e9..eea67588 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 2
+ PrintStmtList body 4
let PrintMember m =
match m with
diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer index 920c87e0..2b7ab098 100644 --- a/Test/jennisys0/Answer +++ b/Test/jennisys0/Answer @@ -6,31 +6,25 @@ 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 a[*]
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
@@ -49,25 +43,17 @@ Jennisys, Copyright (c) 2011, Microsoft. class ExtensibleArray[T] {
var Contents: seq[T]
constructor Init()
- {
Contents := []
- }
method Get(i) returns (t)
requires 0 <= i
requires i < |Contents|
- {
t := Contents[i]
- }
method Set(i, t)
requires 0 <= i
requires i < |Contents|
- {
Contents := Contents[i := t]
- }
method Append(t)
- {
Contents := Contents + [t]
- }
}
model ExtensibleArray[T] {
var elements: array[T]
diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen index b7227d25..e6141ab7 100644 --- a/Test/jennisys0/ExtensibleArray.jen +++ b/Test/jennisys0/ExtensibleArray.jen @@ -2,26 +2,18 @@ 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] {
diff --git a/Test/jennisys0/Prog0.jen b/Test/jennisys0/Prog0.jen index cd847846..14f96628 100644 --- a/Test/jennisys0/Prog0.jen +++ b/Test/jennisys0/Prog0.jen @@ -2,31 +2,28 @@ 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 a[*]
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
+ frame xyz * abc * klm
+ mno pqr
invariant x <= x
}
|