Well-definedness failures do not mask subsequent errors

[viper-admin]

Created by @alexanderjsummers on 2017-01-09 16:44 Last updated on 2017-01-10 14:04

In general, a failed assertion gets assumed for the subsequent verification of the current scope. However, if the failure is a well-definedness condition, this doesn't happen, since the well-definedness checks are made in separate branches.

For example, in the following code, the postcondition of m fails as well as the precondition of t:

#!scala

function t(r: Int) : Bool
    requires r > 0
    ensures r > 0
    {
        r > 0
    }
    
method m() 
    ensures t(0)
{}

[viper-admin]

@marcoeilers commented on 2017-01-10 14:04

In some cases, well-definedness conditions are also apparently checked in the wrong order. For example, in the following code, in the precondition of m, Carbon first complains that the precondition of g does not hold, and then complains that the precondition of f does not hold either. Carbon should check the well-formedness of the inner function application first and subsequently assume that it holds, so in this example, Carbon should complain about the precondition of f, but not of g:

function f(x: Int): Int
    requires x > 0
{ x }

function g(x: Int): Int
    requires x > 0

method m(x: Int)
    requires 0 < g(f(x))

[gauravpartha]

@marcoeilers commented on 2017-01-10 14:04

In some cases, well-definedness conditions are also apparently checked in the wrong order. For example, in the following code, in the precondition of m, Carbon first complains that the precondition of g does not hold, and then complains that the precondition of f does not hold either. Carbon should check the well-formedness of the inner function application first and subsequently assume that it holds, so in this example, Carbon should complain about the precondition of f, but not of g:

function f(x: Int): Int
    requires x > 0
{ x }

function g(x: Int): Int
    requires x > 0

method m(x: Int)
    requires 0 < g(f(x))

I opened a new issue for the problem of checking well-definedness in an unexpected order: https://github.com/viperproject/carbon/issues/435