Skip to content

Commit

Permalink
Added inductive predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
Rustan Leino committed May 7, 2015
1 parent 6380ce0 commit 568f543
Show file tree
Hide file tree
Showing 17 changed files with 895 additions and 626 deletions.
3 changes: 3 additions & 0 deletions Source/Dafny/Cloner.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -604,6 +604,9 @@ public Function CloneFunction(Function f, string newName = null) {
if (f is Predicate) {
return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals,
req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);
} else if (f is InductivePredicate) {
return new InductivePredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
} else if (f is CoPredicate) {
return new CoPredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
Expand Down
30 changes: 23 additions & 7 deletions Source/Dafny/Dafny.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1211,7 +1211,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
List<Expression/*!*/> decreases;
Expression body = null;
bool isPredicate = false; bool isCoPredicate = false;
bool isPredicate = false; bool isIndPredicate = false; bool isCoPredicate = false;
bool isFunctionMethod = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
Expand Down Expand Up @@ -1251,23 +1251,36 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
| "..." (. signatureEllipsis = t; .)
)

/* ----- inductive predicate ----- */
| "inductive" "predicate" (. isIndPredicate = true; .)
(. if (mmod.IsGhost) { SemErr(t, "inductive predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
NoUSIdent<out id>
(
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals>
[ ":" (. SemErr(t, "inductive predicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)

/* ----- copredicate ----- */
| "copredicate" (. isCoPredicate = true; .)
(. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
NoUSIdent<out id>
(
[ GenericParameters<typeArgs> ] (. missingOpenParen = true; .)
[ Formals<true, isFunctionMethod, formals> (. missingOpenParen = false; .)
] (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less co-predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the co-predicate takes no additional arguments"); } .)
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals>
[ ":" (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
)

(. decreases = isCoPredicate ? null : new List<Expression/*!*/>(); .)
(. decreases = isIndPredicate || isCoPredicate ? null : new List<Expression/*!*/>(); .)
{ FunctionSpec<reqs, reads, ens, decreases> }
[ FunctionBody<out body, out bodyStart, out bodyEnd>
]
Expand All @@ -1279,17 +1292,20 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
if (isPredicate) {
f = new Predicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);
} else if (isIndPredicate) {
f = new InductivePredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals,
reqs, reads, ens, body, attrs, signatureEllipsis);
} else if (isCoPredicate) {
f = new CoPredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals,
reqs, reads, ens, body, attrs, signatureEllipsis);
reqs, reads, ens, body, attrs, signatureEllipsis);
} else {
f = new Function(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
}
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
theBuiltIns.CreateArrowTypeDecl(formals.Count);
if (isCoPredicate) {
if (isIndPredicate || isCoPredicate) {
// also create an arrow type for the corresponding prefix predicate
theBuiltIns.CreateArrowTypeDecl(formals.Count + 1);
}
Expand Down
47 changes: 35 additions & 12 deletions Source/Dafny/DafnyAst.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2882,7 +2882,7 @@ public bool AllowsNontermination {
}

/// <summary>
/// The "AllCalls" field is used for non-CoPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for CoPredicate and PrefixPredicate functions).
/// The "AllCalls" field is used for non-FixpointPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for FixpointPredicate and PrefixPredicate functions).
/// It records all function calls made by the Function, including calls made in the body as well as in the specification.
/// The field is filled in during resolution (and used toward the end of resolution, to attach a helpful "decreases" prefix to functions in clusters
/// with co-recursive calls.
Expand Down Expand Up @@ -2972,36 +2972,35 @@ public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isProtecte
}

/// <summary>
/// An PrefixPredicate is the inductive unrolling P# implicitly declared for every copredicate P.
/// An PrefixPredicate is the inductive unrolling P# implicitly declared for every fixpoint-predicate P.
/// </summary>
public class PrefixPredicate : Function
{
public override string WhatKind { get { return "prefix predicate"; } }
public readonly Formal K;
public readonly CoPredicate Co;
public readonly FixpointPredicate FixpointPred;
public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,
List<TypeParameter> typeArgs, Formal k, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, Attributes attributes, CoPredicate coPred)
Expression body, Attributes attributes, FixpointPredicate fixpointPred)
: base(tok, name, hasStaticKeyword, isProtected, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {
Contract.Requires(k != null);
Contract.Requires(coPred != null);
Contract.Requires(fixpointPred != null);
Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);
K = k;
Co = coPred;
FixpointPred = fixpointPred;
}
}

public class CoPredicate : Function
public abstract class FixpointPredicate : Function
{
public override string WhatKind { get { return "copredicate"; } }
public readonly List<FunctionCallExpr> Uses = new List<FunctionCallExpr>(); // filled in during resolution, used by verifier
public PrefixPredicate PrefixPredicate; // filled in during resolution (name registration)

public CoPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
Expression body, Attributes attributes, IToken signatureEllipsis)
public FixpointPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
Expression body, Attributes attributes, IToken signatureEllipsis)
: base(tok, name, hasStaticKeyword, isProtected, true, typeArgs, formals, new BoolType(),
req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis) {
}
Expand Down Expand Up @@ -3036,6 +3035,30 @@ public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Express
}
}

public class InductivePredicate : FixpointPredicate
{
public override string WhatKind { get { return "inductive predicate"; } }
public InductivePredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
Expression body, Attributes attributes, IToken signatureEllipsis)
: base(tok, name, hasStaticKeyword, isProtected, typeArgs, formals,
req, reads, ens, body, attributes, signatureEllipsis) {
}
}

public class CoPredicate : FixpointPredicate
{
public override string WhatKind { get { return "copredicate"; } }
public CoPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
Expression body, Attributes attributes, IToken signatureEllipsis)
: base(tok, name, hasStaticKeyword, isProtected, typeArgs, formals,
req, reads, ens, body, attributes, signatureEllipsis) {
}
}

public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext
{
public override string WhatKind { get { return "method"; } }
Expand Down
Loading

0 comments on commit 568f543

Please sign in to comment.