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
Facility PushDemo;
uses String_Theory;
Facility Integer_Stack_Fac is Stack_Template(Integer, 5)
realized by Array_Realiz;
Operation MyPush(preserves I: Integer; updates S: Stack);
ensures (|#S| < 5 and S = <#I> o #S) or |#S| = 5 and S = #S;
Procedure
Var J: Integer;
J := I;
If Depth(S) + 1 <= 5 then
Push(J, S);
end;
end;
Operation Main();
Procedure
end Main;
end;
Another example where the prover fails to complete:
The text was updated successfully, but these errors were encountered:
Out of scope for our team (at least for now). Original ticket is from November 5, 2015. It has been updated since then, but it does not seem like the issue is officially fixed, as it is now part of the complete prover refactor.
Uh oh!
There was an error while loading. Please reload this page.
Facility PushDemo;
uses String_Theory;
Facility Integer_Stack_Fac is Stack_Template(Integer, 5)
realized by Array_Realiz;
Operation Main();
Procedure
end Main;
end;
Another example where the prover fails to complete:
The text was updated successfully, but these errors were encountered: