On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad wrote:
> 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.

Right. So if X is false, the axiom we declare is !P, not "false" or "a fallacy".

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

That's ok. There is no contradiction if P is false.

False => X is true for any X, so the axiom we declare is just a tautology.


So is the control flow definition / unreachability argument clear now?


> > 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"…

I don't get this part, maybe you can reword it if I haven't already answered the question.

On Thursday, 7 August 2014 at 07:57:14 UTC, Johannes Pfau wrote:
>> 
>> Attempting to continue operating is irresponsible if the program is doing or can do anything important.
>
> Again: unittests?

unittests shouldn't use assert.  Or alternately, we can have onAssertError (the assertion failure callback) do something different if unit testing is taking place than when the program is actually running.

On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
> Right. So if X is false, the axiom we declare is !P, not "false" or "a fallacy".

But Pn is always true where you assume…?

> False => X is true for any X, so the axiom we declare is just a tautology.

I don't follow. If any assumption is false then anything goes…

> So is the control flow definition / unreachability argument clear now?

Nope.

>> > 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"…
>
> I don't get this part, maybe you can reword it if I haven't already answered the question.

assume(true)
r = calc()
assert(specification_test(r)) //required to hold for any situation

assume(false)
r=calc()
//r can be anything


// input!=0
assume(input!=0) // true
r=calc(input)
assert(specification(input)==r) // required to hold for input!=0


//input=0
assume(input!=0)  // false
r=calc(input)
assert(specification(input)==r) // may or may not hold

On 8/7/14, 9:51 AM, Sean Kelly wrote:
> On Thursday, 7 August 2014 at 07:57:14 UTC, Johannes Pfau wrote:
>>>
>>> Attempting to continue operating is irresponsible if the program is
>>> doing or can do anything important.
>>
>> Again: unittests?
>
> unittests shouldn't use assert.  Or alternately, we can have
> onAssertError (the assertion failure callback) do something different if
> unit testing is taking place than when the program is actually running.

Considering that TDPL, Ali's Book[1] and dlang.org[2] all use assert when introducing unittest, I think the latter solution is probably the right one.

[1] http://ddili.org/ders/d.en/unit_testing.html
[2] http://dlang.org/unittest.html

On Thursday, 7 August 2014 at 15:21:14 UTC, H. S. Teoh via Digitalmars-d wrote:
>
> 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.

I suspect this new treatment of assert will affect the way that people check for errors.  For example, in the server apps I write, I don't always want a hard stop of the entire process if I detect a logic error because it provides a potential attack vector for a user to bring down an entire service.  As soon as someone determines that a particular request kills all transactions on a process...

This isn't just paranoia in a new direction either.  The servers I work on are literally under constant attack by hackers.  Largely botnets trying to crack passwords, but not exclusively that.  And so I might want to at least drain out all pending requests before halting the process, or I might want to just kill the transaction that detected the logic error and leave everything running, assuming I can be sure that the potential collateral damage is local to the transaction (which is typically the case).

Longer term, this new treatment of assert will probably encourage better program design which guarantees memory isolation by multiprocessing.  I favor this direction, but messaging has a way to go first.  And by extension, I do think that memory sharing in a language that allows direct memory access is the real risk.  That a logic error might cause a thread / process to generate an invalid message is not an issue any more than it would be an issue to call a function with bad parameters.  In both cases, the implication is that the caller is in an invalid state, not the callee.  So long as there is no vector through which one context can alter the data accessed by another context without proper validation, the corruption cannot spread.

On Thursday, 7 August 2014 at 16:56:01 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
>> Right. So if X is false, the axiom we declare is !P, not "false" or "a fallacy".
>
> But Pn is always true where you assume…?

No. Remember P is "control flow can reach this assume". If the assume is unreachable, then P is false. The compiler doesn't always know that P is false though, so we can use assume(false) to supply that as an axiom.

Here's an example:

x = rand() & 3; // x is 0,1,2 or 3.
switch(x) {
  case 0: foo();
  case 1: bar();
  case 2: baz();
  case 3: qux();
  default: assume(false); // hopefully redundant with a decent compiler.
}

now the compiler can optimize this down to

{foo, bar, baz, qux}[x]();

or even better, a computed jump.

>
>> False => X is true for any X, so the axiom we declare is just a tautology.
>
> I don't follow. If any assumption is false then anything goes…
>

Using my definition of assume, the axiom declared is P=>x. If P is false, then the axiom declared is false => x, which is true for any x.

http://en.wikipedia.org/wiki/Truth_table#Logical_implication


>> So is the control flow definition / unreachability argument clear now?
>
> Nope.

Ok, is it clear now? If not, which parts are not clear?

"H. S. Teoh via Digitalmars-d"  wrote in message news:mailman.674.1407424873.16021.digitalmars-d@puremagic.com...

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

I meant asserts in pre-conditions when used with inheritance.  It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last. 

On Fri, Aug 08, 2014 at 03:44:06AM +1000, Daniel Murphy via Digitalmars-d wrote:
> "H. S. Teoh via Digitalmars-d"  wrote in message news:mailman.674.1407424873.16021.digitalmars-d@puremagic.com...
> 
> >> 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.
> 
> I meant asserts in pre-conditions when used with inheritance.  It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.

Oh, I see it now.

Hmph. Now it's making me wonder if preconditions should be treated as a *single* assert outside the body of 'in{}', rather than allowing individual asserts inside. Perhaps the body of 'in{}' should return a boolean where false indicates a failed precondition, so that instead of writing:

	auto func(...)
	in {
		assert(cond1);
		assert(cond2);
		assert(cond3);
	}
	body { ... }

you'd write instead:

	auto func(...)
	in { cond1 && cond2 && cond3 }
	body { ... }

and the compiler translates this to:

	bool __func__in(...) { return cond1 && cond2 && cond3; }
	auto func(...) {
		assert(__func_in(...));
		// body goes here
	}

Well, technically it should be the caller that invokes __func_in(), but
that's a different issue.


T

-- 
We are in class, we are supposed to be learning, we have a teacher... Is it too much that I expect him to teach me??? -- RL

On Thursday, 7 August 2014 at 17:38:22 UTC, David Bregman wrote:
> Using my definition of assume, the axiom declared is P=>x. If P is false, then the axiom declared is false => x, which is true for any x.

I don't see how this will work out. If it is truly unreachable then you don't need any assume, because then you can assert anything. Therefore you shouldn't.

valid:

assume(true)
while(true){}
assert(angels_love_pixiedust) //proven true now…

But there are alternatives to HL that I don't know much about. You might want to look at "Matching Logic Reachability". Looks complicated:

http://fsl.cs.illinois.edu/pubs/rosu-stefanescu-2012-fm.pdf


> Ok, is it clear now? If not, which parts are not clear?

It doesn't make any sense to me since I don't see how you would discriminate between your Ps.

{P1}
while(true) skip; endwhile
{P2}

How do you define P1 and P2 to be different?

On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad wrote:
> I don't see how this will work out. If it is truly unreachable then you don't need any assume

I just gave you a concrete example of where assume(false) might be useful for optimizing a switch statement. Just because it is truly unreachable doesn't mean the compiler is aware of that.

>
> It doesn't make any sense to me since I don't see how you would discriminate between your Ps.
>
> {P1}
> while(true) skip; endwhile
> {P2}
>
> How do you define P1 and P2 to be different?

I'm not sure how you'd define them to be the same. They're different lines of code, for one thing.