On Thursday, 7 August 2014 at 08:52:43 UTC, Matthias Bentrup wrote:
>
> So reachability has an influence, but control flow hasn't ?

You have to define what you want to prove.

1. The post condition to hold?

2. A sound specification to be fully implemented?

3. That executed code is tested when it executes, but ignore that important code should have been executed instead.

(1) and (2) is what program verification and aims for.
(1) is what design by contract tries to establish.
(3) is weak and what c-asserts do.

On 8/7/2014 12:54 AM, Johannes Pfau wrote:
> Again: unittests?

Asserts in unittests are not the same as asserts elsewhere. I wasn't a big fan of this, but I was probably the only one :-)

On 8/7/2014 2:10 AM, "Marc Schütz" <schuetzm@gmx.net>" wrote:
> 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.

No, all the threads. Threads share memory, so corruption can spread from one to the next.

"Walter Bright"  wrote in message news:lrvglk$25dt$1@digitalmars.com...

> Asserts in unittests are not the same as asserts elsewhere. I wasn't a big fan of this, but I was probably the only one :-)

This has the fun side-effect that asserts in unittest helper functions are fatal, while ones in the unittest body are not!

And we've also got asserts in pre-conditions, which are recoverable by definition. 

On Thursday, 7 August 2014 at 09:26:01 UTC, Walter Bright wrote:
> On 8/7/2014 2:10 AM, "Marc Schütz" <schuetzm@gmx.net>" wrote:
>> 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.
>
> No, all the threads. Threads share memory, so corruption can spread from one to the next.

Yes, that's what I was saying: "those threads ... that ha[ve] access to memory shared with that failed thread".

But even without real sharing of memory, a failed assertion in one thread might result from invalid data being sent to that thread from another one (via spawn or send). Better to just kill all threads.

On Wednesday, 6 August 2014 at 22:31:00 UTC, Walter Bright wrote:
> 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.

But for those 30 years you only used asserts with the semantics they have in C, not with the semantics you want for D. I don't see how you can come to the conclusion that the same is true for the "new style" assertions.

The problems with finding errors that I talk about are not because the cause of the error is far from the assert. They stem from the fact that - with the proposed semantics - the asserts themselves can influence code in different parts of the program, far away from both the cause of the error and the failed assert.

On Thursday, 7 August 2014 at 07:53:44 UTC, Ola Fosheim Grøstad wrote:
> 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?

If you use the definition of assume that I gave, assume(P && false) declares the axiom

P => (P && false)

which is again equivalent to !P.

On Thu, Aug 07, 2014 at 07:29:43PM +1000, Daniel Murphy via Digitalmars-d wrote:
> "Walter Bright"  wrote in message news:lrvglk$25dt$1@digitalmars.com...
> 
> >Asserts in unittests are not the same as asserts elsewhere. I wasn't a big fan of this, but I was probably the only one :-)
> 
> This has the fun side-effect that asserts in unittest helper functions are fatal, while ones in the unittest body are not!
> 
> And we've also got asserts in pre-conditions, which are recoverable by definition.

Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function.


T

-- 
Answer: Because it breaks the logical sequence of discussion. Question: Why is top posting bad?

On Thursday, 7 August 2014 at 14:09:26 UTC, David Bregman wrote:
> If you use the definition of assume that I gave, assume(P && false) declares the axiom
>
> P => (P && false)
>
> which is again equivalent to !P.

Well, P=>(P&&X) is equivalent to P=>X.

But you are allowed to have "false" in the preconditions, since we only are interested in

preconditions => postconditions

assume(input!=0) is ok… it does not say unreachable.
It says, postconditions are not required to hold for input==0…

On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad wrote:
> assume(input!=0) is ok… it does not say unreachable.
> It says, postconditions are not required to hold for input==0…

And… assume(false) is a precondition that says that you don't have to care about the postconditions at all… Basically, "assume anything"…