On Thursday, 7 August 2014 at 03:51:02 UTC, Ola Fosheim Grøstad
wrote:
> 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.

But control flow can introduce mathematical dependencies. E.g.
for assert the code

   if(a) {
     assert(b);
     ...
   }

is not equivalent to

   assert(b);
   if(a) {
     ...
   }

but not because the assertion depends on a different incarnation
of "b", but because it also depends on "a", so it is like

   assert(!a || b);
   if(a) {
     ...
   }

If assume is independent of control flow, then clearly this
cannot be related to assert. But I think the proposal was not to
replace assert with the textbook definition of assume, rather to
use the information in asserts to optimize the code. So if assume
doesn't work, what about assume_here() ?

On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim Grøstad wrote:
> «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?

It doesn't have to be a special case if you define it in the right way - in terms of control flow. Then the interpretation of assume(false) as unreachable follows quite naturally:

instead of defining assume(x) to mean that x is an axiom, define assume(x) to mean that P=>x is an axiom, where P is the proposition that control flow reaches the assume statement.

so assume(false) actually means P=>false, or simply !P

and !P means !(control flow reaches the assume), as desired.

On Thursday, 7 August 2014 at 05:41:22 UTC, Matthias Bentrup wrote:
> If assume is independent of control flow, then clearly this
> cannot be related to assert.

Well, both assume and assert are "independent" of control flow since you don't have execution or control flow in mathematics.

The dependency is tied to the "renaming of variables into constants" which allows Hoare-Logic to work on variables, not only constants. However, for proper constants, you don't need that limit for neither assert nor assume?

if(B){
   assume(B && PI==3.14)
} else {
   assume(!B && PI==3.14) // must hold here too since it is a constant
}

apply hoare logic rule for if:

if this holds:

{B ∧ P} S {Q}   ,   {¬B ∧ P } T {Q}

then this holds:

{P} if B then S else T endif {Q}

which gives:

assume(PI==3.14)
f(B){
   assume(PI==3.14)
} else {
   assume(PI==3.14)
}
assume(PI==3.14)


(Usually you only have assume at the top in the preconditions, since you otherwise don't get a proof :-).

On Thursday, 7 August 2014 at 06:04:38 UTC, David Bregman wrote:
> On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim Grøstad wrote:
>> «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?
>
> It doesn't have to be a special case if you define it in the right way - in terms of control flow. Then the interpretation of assume(false) as unreachable follows quite naturally:
>
> instead of defining assume(x) to mean that x is an axiom, define assume(x) to mean that P=>x is an axiom, where P is the proposition that control flow reaches the assume statement.
>
> so assume(false) actually means P=>false, or simply !P
>
> and !P means !(control flow reaches the assume), as desired.

Let's try the opposite way instead:

assume(Q)
if(B1){
   if(B2){
   }
}

implies:

assume(Q)
if(B1){
   assume(B1&&Q)
   if(B2){
      assume(B1&&B2&&Q)
   }
}

So your P in the inner if statement is  B1&&B2.

However assume(P&&false) is still a fallacy…

Or?

Am Wed, 06 Aug 2014 20:19:33 -0700
schrieb Walter Bright <newshound2@digitalmars.com>:

> 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.
> 
> 

I can see some benefits here, but how does this interact with asserts in unittests? You might special-case these, but it's also common practice to use these asserts not only in the main unittest function but also in helper functions.

Am Wed, 06 Aug 2014 14:57:50 -0700
schrieb Walter Bright <newshound2@digitalmars.com>:

> On 8/6/2014 10:18 AM, Sean Kelly wrote:
> > So from a functional perspective, assuming this is a multithreaded app, what should the procedure be when an AssertError is thrown in some thread?
> 
> Print message, stop the process and all its threads.
> 
> Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread.
> 
> Attempting to continue operating is irresponsible if the program is doing or can do anything important.

Again: unittests?

On Thursday, 7 August 2014 at 06:32:18 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 7 August 2014 at 05:41:22 UTC, Matthias Bentrup wrote:
>> If assume is independent of control flow, then clearly this
>> cannot be related to assert.
>
> Well, both assume and assert are "independent" of control flow since you don't have execution or control flow in mathematics.
>
> The dependency is tied to the "renaming of variables into constants" which allows Hoare-Logic to work on variables, not only constants. However, for proper constants, you don't need that limit for neither assert nor assume?
>
> if(B){
>    assume(B && PI==3.14)
> } else {
>    assume(!B && PI==3.14) // must hold here too since it is a constant
> }
>
> apply hoare logic rule for if:
>
> if this holds:
>
> {B ∧ P} S {Q}   ,   {¬B ∧ P } T {Q}
>
> then this holds:
>
> {P} if B then S else T endif {Q}
>
> which gives:
>
> assume(PI==3.14)
> f(B){
>    assume(PI==3.14)
> } else {
>    assume(PI==3.14)
> }
> assume(PI==3.14)
>
>
> (Usually you only have assume at the top in the preconditions, since you otherwise don't get a proof :-).

So the D function (note that "a" is constant)

int silly() {
  enum int a = 1;
  if( a == 2 ) {
    assert( a == 2 );
  }
  return a;
}

has undefined semantics (at least in debug mode), because it contains a false assertion ?

That is not my understanding of assert.

On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup wrote:
> So the D function (note that "a" is constant)
>
> int silly() {
>   enum int a = 1;
>   if( a == 2 ) {
>     assert( a == 2 );
>   }
>   return a;
> }
>
> has undefined semantics (at least in debug mode), because it contains a false assertion ?

It isn't reachable so it is not part of the program? If you support generic programming you probably should limit proofs to reachable portions of library code.

However the specification or the implementation of it appears to be flawed, so perhaps it should be considered incorrect if this was in application code.

You usually try to prove post conditions in terms of pre conditions. The invariants, variants and asserts are just tools to get there. So this is not a typical issue.

On Thursday, 7 August 2014 at 08:35:21 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup wrote:
>> So the D function (note that "a" is constant)
>>
>> int silly() {
>>  enum int a = 1;
>>  if( a == 2 ) {
>>    assert( a == 2 );
>>  }
>>  return a;
>> }
>>
>> has undefined semantics (at least in debug mode), because it contains a false assertion ?
>
> It isn't reachable so it is not part of the program? If you support generic programming you probably should limit proofs to reachable portions of library code.
>
> However the specification or the implementation of it appears to be flawed, so perhaps it should be considered incorrect if this was in application code.
>
> You usually try to prove post conditions in terms of pre conditions. The invariants, variants and asserts are just tools to get there. So this is not a typical issue.

So reachability has an influence, but control flow hasn't ?

On Wednesday, 6 August 2014 at 21:57:50 UTC, Walter Bright wrote:
> On 8/6/2014 10:18 AM, Sean Kelly wrote:
>> So from a functional perspective, assuming this is a multithreaded app, what
>> should the procedure be when an AssertError is thrown in some thread?
>
> Print message, stop the process and all its threads.
>
> Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread.

Strictly speaking we would need to kill only those threads. But I guess it wouldn't be worth the effort, because the remaining threads are most likely not expecting them to disappear and couldn't recover from this.