Jessie is not able to prove the post-condition. Why?
• A lot of work has been done on floating-point operations since the last release. That is to say, support for floating-point operations will be much less partial in the next release than in Lithium, both for Jessie and for the Value Analysis. • With the value analysis you need to indicate that the property must be analyzed by case by adding an assertion x⇐0 || x>=0, which does not incur any additional proof obligation since it can be verified to hold easily. The same trick may help automatic theorem provers, if you somehow arrange for this disjunction to be in the hypotheses, they may have the idea to study what that means for x*x separately. • With both Jessie or the Value Analysis you will get a proof obligation. You will probably want to use the “strict” model in which infinites and NaN are treated as unwanted errors when they occur. In this case the proof obligation is that x*x should not overflow. So, in the previous example, even with the full model in Jessie your post-condition
Related Questions
- What criteria must be met for an individual to prove they are a member of a Métis community and are able to exercise that communitys Aboriginal right?
- How do we prove to the evaluators we are able to provide the required training to the awareness nodes?
- What must a material supplier be able to prove in order to claim a lien?
