Refinement across files doesn't check post condition

Apr 16, 2014 at 11:19 AM
In a file abstract_module.dfy I have the following abstract module:
abstract module Abstract
{
    static function method inc(x:int) :int
        ensures inc(x) > x;
}
In another file I have the following concrete module:
include "abstract_module.dfy"

module Concrete refines Abstract
{
    static function method inc...
    {
        x - 1
    }
}
I expected Dafny to fail to verify the function inc in the concrete module, however it gives no error message in the VS extension or on the command line. From the command line, I see:
Dafny program verifier version 1.8.1.10324, Copyright (c) 2003-2014, Microsoft.

Dafny program verifier finished with 0 verified, 0 errors
From the "0 verified" I deduce that Dafny does not import the specification from the abstract into the concrete module, even though the VS tool tip shows the correct specification on the refined function.

If I put both modules in the same file then I get the error message that I anticipated:
Dafny program verifier version 1.8.1.10324, Copyright (c) 2003-2014, Microsoft.
abstract_module.dfy(8,25): Error BP5003: A postcondition might not hold on this return path.
abstract_module.dfy(4,18): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else

Dafny program verifier finished with 1 verified, 1 error
Have I misunderstood how module refinement is supposed to work in this situation? I was hoping to use this feature to split up my proof, as I am having problems with Dafny timing out when it is all in a single file.

Cheers,

Tim
Apr 16, 2014 at 6:37 PM
In the VS tooltip I have noticed it adds "{:verify false}" to the function definition in the file containing the concrete module. Presumably this is intended to prevent the included function from being verified twice, but perhaps in this case it is not necessary, since the abstract function has no body and so was not previously verified?
Apr 16, 2014 at 6:58 PM
Perhaps in Parser.cs "FunctionDecl" it can check if the "body != null" before it adds the ":verify false" attribute? Like
if (!theVerifyThisFile && body != null) {  // We still need the func bodies, but don't bother verifying their correctness
     List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
     Attributes.Argument/*!*/ anArg;
     anArg = new Attributes.Argument(id, new LiteralExpr(t, false));
     args.Add(anArg);
     attrs = new Attributes("verify", args, attrs);
}
and also in similarly "MethodDecl"
if (!theVerifyThisFile && body != null) {
    body = null;
         
    List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
    Attributes.Argument/*!*/ anArg;
    anArg = new Attributes.Argument(id, new LiteralExpr(t, false));
    args.Add(anArg);
    attrs = new Attributes("verify", args, attrs);
}
Apr 18, 2014 at 9:00 AM
It occurs to me that the solution I proposed above does not cover the case where a function with a body is refined in a derived module.

Thinking about it a bit more, it seems that the (some/all) attributes are being attached to the wrong element. They are being attached to the function declaration, but really they are meaningful only for the function body. Take for example

:verify - means verify or not the function body
:induction - means use induction or not to prove the body
:opaque - means expose the body or not
:timeout - means use a particular timeout when verifying the body

None of the above really make sense for functions/methods with no body. And it seems to me also, that it doesn't make too much sense to have them inherited onto refining implementations. If we decide to disable induction for a particular method body, that does not necessarily mean we should disable it for any refining method body.

So perhaps instead of writing something like
static lemma {:verify false} strictlySmallerMapHasFewerElementsInItsDomain<U,V>(m: map<U,V>, m': map<U,V>)
        requires mapSmaller(m,m') && m != m';
        ensures domain(m') - domain(m) != {};
{
   // stuff
}
We could write something that puts the annotations on the body, like perhaps this:
static lemma strictlySmallerMapHasFewerElementsInItsDomain<U,V>(m: map<U,V>, m': map<U,V>)
        requires mapSmaller(m,m') && m != m';
        ensures domain(m') - domain(m) != {};
{:verify false} 
{
   // stuff
}
Coordinator
Apr 20, 2014 at 3:02 AM
Hi Tim,

Thanks for finding and analyzing this problem. It seems to stem from an inconsistency between how include says not to verify the contents of the included file and how the refinement features inherit code. I have now changed the implementation to no longer use the {:verify false} attribute, but to instead mark the source-location tokens internally (see change set eaedc894f0be). I hope that works. Shout if it doesn't.

Rustan
Marked as answer by rustanleino on 5/3/2014 at 9:18 AM
Apr 27, 2014 at 11:27 AM
Thanks Rustan, that seems to be working well.

Cheers,

Tim