← Back to context

Comment by ngruhn

21 hours ago

How would that look like if you accidentally assumed you have arbitrary large integers but in practice you have 64 bits?

10 comments

ngruhn

Reply
appellations  20 hours ago 

    Add(x,y):
       Assert( x >= 0 && y>= 0 )
        z = x + y
        Assert( z >= x && z >= y )
        return z

There’s definitely smarter ways to do this, but in practice there is always some way to encode the properties you care about in ways that your assertions will be violated. If you can’t observe a violation, it’s not a violation https://en.wikipedia.org/wiki/Identity_of_indiscernibles

  • bluGill  19 hours ago

    In some languages overflow is asserted as a can't happen and so the optimizer will remove your checks

    • appellations  17 hours ago

      Best I can tell is that overflow is undefined behavior for signed ints in C/C++ so -O3 with gcc might remove a check that could only be true if UB occurred.

      The compound predicate in my example above coupled with the fact that the compiler doesn’t reason about the precondition in the prior assert (y is non-negative) means this specific example wouldn’t be optimized away, but bluGill does have a point.

      An example of an assert that might be optimized away:

          int addFive(int x) {
        int y = x + 5;
        assert(y >= x);
        return y;
    }

      2 replies →