On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
> On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
>>
>> Ah, I had a different understanding of assume, i.e. placing an
>> assume(A) at some point in code adds not the axiom A, but rather
>> the axiom "control flow reaches this spot => A".
>
> (Your understanding is the conventional one.)

Yeah, the one with control flow is really the only useful way to define it, at least for use in an imperative language. If you can only write assumes which are globally valid, then you can't refer to local variables in the expression. That makes it pretty useless.

As for assume(0), in the control flow interpretation it makes perfect sense: Assuming control flow reaches here, false = true. So by contradiction, "control flow reaches here" is false, i.e. that point is unreachable.

see again the __assume extension in the Microsoft c++ compiler: http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx

On Wednesday, 6 August 2014 at 21:35:26 UTC, Sean Kelly wrote:
> On Wednesday, 6 August 2014 at 21:16:42 UTC, David Bregman wrote:
>> On Wednesday, 6 August 2014 at 20:27:45 UTC, Sean Kelly wrote:
>>> Well, it seems like the underlying idea is to treat assertion failures more strongly than we do now.  So changes in how these are handled by the runtime might be a side effect of this proposal.
>>
>> Again, since Walter's proposal only affects release mode, I don't see how exceptions or the runtime are related. What am I missing? You agree assertion failures (AssertError) are only thrown in debug mode, right?
>
> In non-release mode, but yes.  However:
>
> 4. An assert failure is a non-recoverable error. The compiler may assume that
> execution does not proceed after one is tripped. The language does allow
> attempts to shut a program down gracefully after one is tripped, but that must
> not be misconstrued as assuming that the program is in a valid state at that point.
>
> 5. assert(0); is equivalent to a halt, and the compiler won't remove it.
>
>
> Clearly, the intention is for assertion failures to terminate the program, but that isn't done now.  Or at least this isn't done in the multithreaded case.  So I was asking for clarification on what should be done on that end, and whether that behavior should inform how assert is treated from a language perspective.

Ah, ok. So it's an issue with the existing implementation not matching some other expectations, not related to the main topic of this thread. Sorry for the confusion.

Anyway, Walter just replied to your first post, I'll defer to him on this.

On 08/06/14 22:57, via Digitalmars-d wrote:
> On Wednesday, 6 August 2014 at 17:36:00 UTC, Artur Skawina wrote:
>>    if (0)
>>       assume(0);
>>
>> Yes, `assume` could be defined in a way that would make this always a compile error. But then `assume(0)` would be useless.
> 
> I don't think so. It makes a lot of sense to halt compilation if you from templates or other constructs emit assume(true==false) or assert(true==false) or any other verification-annotation that contradicts predefined language axioms in a way that the compiler can detect at compile time. Otherwise you risk having "unreachable" unintended in generic code.

D already has `static assert`, which can be used for compile-time checks. Eliminating unreachable paths based on the extra information from (a combination of) `assume` statements is desirable, and exactly what this thread is about.

I get what you're saying, but it's not really relevant in the context
of `D`; such fundamental changes are not exactly likely to happen soon...
OTOH the extremely dangerous assert->assume redefinition seems to be
seriously considered, despite the grave consequences...

artur

On 8/6/2014 5:14 AM, "Marc Schütz" <schuetzm@gmx.net>" wrote:
> We're not living in an ideal world, unfortunately. It is bad enough that
> programs are wrong as they are written, we don't need the compiler to transform
> these programs to do something that is still wrong, but also completely
> different. This would make your goal of fixing the program very hard to achieve.
> In an extreme case, a small error in several million lines of code could
> manifest at a completely different place, because you cannot rely on any
> determinism once undefined behaviour is involved.

You are technically correct, and I used to worry about that. But after using assert()s for 30 years, I can only think of this happening once. assert()s tend to trip very shortly after the actual error occurred. Of course, there's a bit of an art to appropriate placement of those assert()s.


> It seems like
> the opposite: instead of trying to prove the assertions statically, they're
> going to be believed without verification.

The point of an assert is it is something the programmer says must be true, not the compiler.

On Wednesday, 6 August 2014 at 22:01:47 UTC, Walter Bright wrote:
> On 8/6/2014 12:34 PM, Sean Kelly wrote:
>> There is no facility for forcing a clean termination of another
>> thread.
>
> Understood - so the only option is to force an unclean termination.

So in all cases, it seems like what we should be doing is call exit(1) or the equivalent and forego any attempt at cleanup.  Otherwise an assertion failure in a spawned thread would be handled even more strongly than in the main thread.

Alternately, if we build on std.concurrency we could have the next call to receive throw a FatalError or something to force it to terminate.  But there's no telling how long this would be.  I assume you prefer the forceful route.


> Let me emphasize that when an assert trips, the program has failed. It is in an invalid, unknown, indeterminate state from that moment forward.

I think in many cases the scope of possible invalid states can actually be determined given a reasonable understanding of the program.  For example, if a thread within a @safe app encounters an error, it might be possible to assert that the damage does not extend beyond the limits of data referenced by the thread.  But I do appreciate the desire to not deal lightly with detected logic errors so I won't push the point.

> Use enforce() for errors that are anticipated and cleanly recoverable, not assert().

Given what I said above, I'm inclined to say that enforce() should be used by in contracts and the like rather than assert(), and to save assert() for the situations where I'm certain there's absolutely nothing to be done.  However, I think of enforce() to be more for run-time problems that might be corrected by trying again later with the same input.  I'll have to give this some thought.

On 8/6/2014 5:22 PM, Sean Kelly wrote:
> On Wednesday, 6 August 2014 at 22:01:47 UTC, Walter Bright wrote:
>> On 8/6/2014 12:34 PM, Sean Kelly wrote:
>>> There is no facility for forcing a clean termination of another
>>> thread.
>>
>> Understood - so the only option is to force an unclean termination.
>
> So in all cases, it seems like what we should be doing is call exit(1) or the
> equivalent and forego any attempt at cleanup. Otherwise an assertion failure in
> a spawned thread would be handled even more strongly than in the main thread.
>
> Alternately, if we build on std.concurrency we could have the next call to
> receive throw a FatalError or something to force it to terminate.  But there's
> no telling how long this would be.  I assume you prefer the forceful route.

Yes, I prefer that.


>> Let me emphasize that when an assert trips, the program has failed. It is in
>> an invalid, unknown, indeterminate state from that moment forward.
>
> I think in many cases the scope of possible invalid states can actually be
> determined given a reasonable understanding of the program.  For example, if a
> thread within a @safe app encounters an error, it might be possible to assert
> that the damage does not extend beyond the limits of data referenced by the
> thread.

I can't agree with that, especially not for the standard library.


>> Use enforce() for errors that are anticipated and cleanly recoverable, not
>> assert().
>
> Given what I said above, I'm inclined to say that enforce() should be used by in
> contracts and the like rather than assert(), and to save assert() for the
> situations where I'm certain there's absolutely nothing to be done.  However, I
> think of enforce() to be more for run-time problems that might be corrected by
> trying again later with the same input.  I'll have to give this some thought.

On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
> On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
>>
>> Ah, I had a different understanding of assume, i.e. placing an
>> assume(A) at some point in code adds not the axiom A, but rather
>> the axiom "control flow reaches this spot => A".
>
> (Your understanding is the conventional one.)

Not right.

You need to take into account that assume() provides a mathematical definition, it isn't an imperative. That would make no sense. So there is no control flow, only mathematical dependencies.

You only deal with constants. "Variables" are just a tool for automatic labeling of constants. You would not be able to use logic otherwise.

"Control flow" is embedded in the dependencies and relationships between the constants.

j=0
for(i=0; i<3;++i){j+=i}

Is just a short-hand for:

j0 = 0
i0 = 0
j1 = j0 + i0
i1 = 1
j2 = j1 + i1
i2 = 2
j3 = j2 + i2

If you map this out as a graph you get the dependencies (mirroring "control flow").

Hoare-logic provide means to reason about the short-hand notation and make transformations on it.

What is unconventional about this?

On Wednesday, 6 August 2014 at 22:03:11 UTC, David Bregman wrote:
> As for assume(0), in the control flow interpretation it makes perfect sense: Assuming control flow reaches here, false = true. So by contradiction, "control flow reaches here" is false, i.e. that point is unreachable.
>
> see again the __assume extension in the Microsoft c++ compiler: http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx

From the docs:
«The __assume(0) statement is a special case.»

So, it does not make perfect sense. If it did, it would not be a special case?

On Wednesday, 6 August 2014 at 22:28:08 UTC, Artur Skawina via Digitalmars-d wrote:
> D already has `static assert`, which can be used for compile-time checks.

The static modifier would just be a modifier to the regular c-style assert that basically tells the compiler to refuse to add run-time checks.

* static assert:  prove this or stop compilation

* assert: prove this or emit runtime check

* assume: define this to hold

> OTOH the extremely dangerous assert->assume redefinition seems to be seriously considered, despite the grave consequences...

Well, I don't worry. It just means that some people, who believe in the concept, are going to spend a lot of effort on something that probably does not pay off. It would be a lot better if they rather spent some effort in adding sound annotations, like bearophile argues for, though. It could be put it to good use by annotating foreign functions

Keep in mind that this is an issue that is easy to fix in a private fork. It is a small modification to turn "d-assert" into "assume" and add a "c-assert". It requires no changes to D code?

I'll also add that perhaps a source of confusion is that assert(X) is presumed to take a bool at compile time. That is not the case, there are 3 outcomes:

X==true : this has been proved to hold

X==false: this has been proved to not hold

X not computable: too weak theorem prover, check at runtime