diff options
Diffstat (limited to 'Test/dafny1/Substitution.dfy')
| -rw-r--r-- | Test/dafny1/Substitution.dfy | 45 |
1 files changed, 20 insertions, 25 deletions
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 8d51bdd1..ad39e3f2 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -1,27 +1,23 @@ -datatype List {
- Nil;
- Cons(Expr, List);
-}
+datatype List = Nil | Cons(Expr, List);
-datatype Expr {
- Const(int);
- Var(int);
+datatype Expr =
+ Const(int) |
+ Var(int) |
Nary(int, List);
-}
static function Subst(e: Expr, v: int, val: int): Expr
{
match e
case Const(c) => e
- case Var(x) => if x == v then #Expr.Const(val) else e
- case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))
+ case Var(x) => if x == v then Expr.Const(val) else e
+ case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
}
static function SubstList(l: List, v: int, val: int): List
{
match l
case Nil => l
- case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))
+ case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
}
static ghost method Theorem(e: Expr, v: int, val: int)
@@ -31,7 +27,7 @@ static ghost method Theorem(e: Expr, v: int, val: int) case Const(c) =>
case Var(x) =>
case Nary(op, args) =>
- call Lemma(args, v, val);
+ Lemma(args, v, val);
}
}
@@ -41,26 +37,25 @@ static ghost method Lemma(l: List, v: int, val: int) match l {
case Nil =>
case Cons(e, tail) =>
- call Theorem(e, v, val);
- call Lemma(tail, v, val);
+ Theorem(e, v, val);
+ Lemma(tail, v, val);
}
}
// -------------------------------
-datatype Expression {
- Const(int);
- Var(int);
+datatype Expression =
+ Const(int) |
+ Var(int) |
Nary(int, seq<Expression>);
-}
static function Substitute(e: Expression, v: int, val: int): Expression
decreases e;
{
match e
case Const(c) => e
- case Var(x) => if x == v then #Expression.Const(val) else e
- case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))
+ case Var(x) => if x == v then Expression.Const(val) else e
+ case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
}
static function SubstSeq(/*ghost*/ parent: Expression,
@@ -80,11 +75,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) case Var(x) =>
case Nary(op, args) =>
ghost var seArgs := SubstSeq(e, args, v, val);
- call LemmaSeq(e, args, v, val);
+ LemmaSeq(e, args, v, val);
ghost var se := Substitute(e, v, val);
ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
- call LemmaSeq(se, seArgs, v, val);
+ LemmaSeq(se, seArgs, v, val);
var N := |args|;
var j := 0;
@@ -92,14 +87,14 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) invariant j <= N;
invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
{
- call TheoremSeq(args[j], v, val);
+ TheoremSeq(args[j], v, val);
j := j + 1;
}
assert seArgs == seArgs2;
}
}
-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)
+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
@@ -107,6 +102,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, {
if (q == []) {
} else {
- call LemmaSeq(parent, q[..|q|-1], v, val);
+ LemmaSeq(parent, q[..|q|-1], v, val);
}
}
|