Menu

#417 Difficulty solving floating point problems

open
None
OpenJML
5
2015-05-26
2015-05-26
David Cok
No

See the code for sfbug414/Sqrt.java - The specs for this are not yet correct. But in particular, it appears the solver has difficulty with even proving x + 1 > x. What is wrong?

Discussion

  • David Cok

    David Cok - 2015-05-26
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -1 +1,3 @@
     See the code for sfbug414/Sqrt.java - The specs for this are not yet correct. But in particular, it appears the solver has difficulty with even proving x + 1 > x. What is wrong?
    +
    +See sfbug411/Sqrt.java as an example
    
     
  • David Cok

    David Cok - 2015-05-26
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -1,3 +1,3 @@
     See the code for sfbug414/Sqrt.java - The specs for this are not yet correct. But in particular, it appears the solver has difficulty with even proving x + 1 > x. What is wrong?
    
    -See sfbug411/Sqrt.java as an example
    +See sfbug414/Sqrt.java as an example
    
     
  • David Cok

    David Cok - 2015-05-26
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -1,3 +1 @@
     See the code for sfbug414/Sqrt.java - The specs for this are not yet correct. But in particular, it appears the solver has difficulty with even proving x + 1 > x. What is wrong?
    -
    -See sfbug414/Sqrt.java as an example
    
     

Log in to post a comment.

MongoDB Logo MongoDB