You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following verifies in Carbon but not in Silicon:
function fac(i: Int): Int
ensures ge(result, 1)
{
i <= 1 ? 1 : i * fac(i - 1)
}
function ge(i1: Int, i2: Int): Bool
{
i1 >= i2
}
The issue is that the precondition propagation axiom for fac (which states that if the precondition of fac is satisfied, then the precondition of ge in its postcondition is also satisfied) is not available while verifying the body of fac, and thus the definition of ge cannot be used when learning the postcondition of the recursive call.
The text was updated successfully, but these errors were encountered:
The following verifies in Carbon but not in Silicon:
The issue is that the precondition propagation axiom for
fac
(which states that if the precondition offac
is satisfied, then the precondition ofge
in its postcondition is also satisfied) is not available while verifying the body offac
, and thus the definition ofge
cannot be used when learning the postcondition of the recursive call.The text was updated successfully, but these errors were encountered: