On 07/31/2014 08:58 PM, Walter Bright wrote:
On 7/31/2014 4:28 AM, David Bregman wrote:
Sigh. Of course you can assume the condition after a runtime check has
been
inserted. You just showed that
assert(x); assume(x);
is semantically equivalent to
assert(x);
as long as the runtime check is not elided. (no -release)
No. I showed that you cannot have an assert without the assume.
No you did not. However:
* You showed that an additional 'assume' would not have any effect if
the check is never elided.
* You showed that the state of knowledge about the program state of the
optimizer are the same after processing a halting runtime check and
after processing an 'assume'.
I don't think anybody is contesting that. Now try to zoom your focus out
a little, and think about _what if_ the assertion and the assumption are
actually wrong? Why does it make sense to conflate them in this case?
That makes them equivalent that direction.
For the other direction, adding in a runtime check for an assume is
going to be expected of an implementation.
Yes if 'assert' does what 'assert' does now, and if 'assume' does what
'assert' does now, then 'assert' and 'assume' do the same. I agree with
that, but the premise is unrelated to this discussion. You are moving
the goal posts.
And, in fact, since the
runtime check won't change the semantics if the assume is correct, they
are equivalent.
...
"If the 'assume'/'assert' are correct" is not a sound assumption to
make. You are not the compiler, you are the programmer. We are
discussing _about_ programs, not _within_ programs.
I.e. for practical purposes, they are the same thing.
All assertions being correct is not a given 'for practical purposes'.
You are arguing in the context of a theoretical ideal and this context
alone.
