On Thu, Aug 07, 2014 at 10:54:53AM -0700, H. S. Teoh via Digitalmars-d wrote:
> 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.
[...]

P.S. The current implementation also does not distinguish between a broken contract vs. a bug or problem encountered by the contract code. For example:

	auto func(T...)(T args)
	in {
		assert(checkConsistency(args));
	}
	body {
		...
	}

	bool checkConsistency(T...)(T args) {
		int i;
		for (i=0; i < args.length; i++) {
			...
			i = 1000; // suppose an inadvertent typo causes this
		}
		assert(i == args.length); // so this will fail
		...
		return result;
	}

Suppose the i=1000 line is a mistake by the programmer, so it's a genuine bug in checkConsistency. This would trip the assert in checkConsistency, which would throw an AssertError. But if it was called from the in-contract of func(), and func() is in a derived class for which the base class version of func() has an in-contract that passes, then we're basically swallowing the AssertError triggered by the failed malloc(), and thereby causing the program to continue running in an invalid state!

Basically, the problem is that the in-contract can't tell the difference
between a precondition failure (triggered by the outer assert) and a
genuine program bug (triggered by the inner assert).

This makes DbC in D really shaky.  :-(


T

-- 
Freedom: (n.) Man's self-given right to be enslaved by his own depravity.

On Thursday, 7 August 2014 at 17:44:02 UTC, Daniel Murphy 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 man, I forgot about this.  I wonder how this works from a codegen perspective.  Is precondition inheritance properly implemented yet?

On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
> On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad wrote:
> I just gave you a concrete example of where assume(false) might be useful for optimizing a switch statement.

But to me it sounds dangerous if it actually is reachable or if the compiler somehow think it is. So you should use halt() if it should be unreachable, and use unreachable() if you know 100% it holds. Encouraging assume(false) sounds like an aberration to me.

You need to provide proofs if you attempt using assume(X) and assert(false).

This is valid, but it is derived, not postulated:

assume(P)
while(false){

   assume(false)  // anything goes is acceptable over S here
   S…         // since it never happens…
   assert(P) // valid since the assumption is false

}
assert(P) // valid since the content is just a noop


When you postulate without proving you open a can of worms:

assume(P)
while(B){

   assume(false)  // woops! Should have been assume(B&&P)
   S…                  // ohoh we just stated anything goes in here…
   assert(P)          // invalid

}
assert(P)  // invalid since the loop invariant doesn't hold.



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

I don't believe there "is" such a thing as lines of code. We are doing math. Everything just "is". We don't have code, we have mathematical dependencies/relations. P1 and P2 are propositions, so what are the content of those? The ones you use for your P1=>X and P2=>Y? You have to define newassume(P,X)===assume(P=>X). But what is P?

Anyway, you don't need those… You can use a regular assume(false), but not for indicating unreachable. You indicate that the postcondition does not have to hold. Otherwise you will run into trouble.

But if you think about while() as a short-hand that is expanded into pure math, then it makes sense. If you have while(true){} then the loop cannot generate new mathematical constants… Thus it cannot be a source for new unique propositions that let you discriminate between before and after entering the loop? Or?

On Thursday, 7 August 2014 at 19:41:44 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
>> On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad wrote:
>> I just gave you a concrete example of where assume(false) might be useful for optimizing a switch statement.
>
> But to me it sounds dangerous if it actually is reachable or if the compiler somehow think it is.

It is dangerous, and shouldn't be used lightly. That's what started this whole thread.

> So you should use halt() if it should be unreachable,

Not if your goal is to completely optimize away any unreachable code.

> and use unreachable() if you know 100% it holds.

This is just another name for the same thing, it isn't any more or less dangerous.

> Encouraging assume(false) sounds like an aberration to me.

If you accept my definition of assume there is no problem with it, it just means unreachable. I showed how this follows naturally from my definition.

>
> You need to provide proofs if you attempt using assume(X) and assert(false).

There is no mechanism for providing proofs or checking proofs in D.

>>> 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.
>
> I don't believe there "is" such a thing as lines of code. We are doing math. Everything just "is". We don't have code, we have mathematical dependencies/relations.

Well, any correct mathematical formalism of the code must preserve its semantics, so it doesn't really matter which one we talk about.

Different lines (or basic blocks, I guess is the right term here) can have different reachability, so you could just give each one its own P.

> P1 and P2 are propositions, so what are the content of those? The ones you use for your P1=>X and P2=>Y?

This is just an implementation detail of the compiler. Probably each basic block has its own P, which is conservatively approximated with some data flow analysis. (Disclaimer: I am not a compiler expert)

> Anyway, you don't need those… You can use a regular assume(false), but not for indicating unreachable. You indicate that the postcondition does not have to hold. Otherwise you will run into trouble.
>
> But if you think about while() as a short-hand that is expanded into pure math, then it makes sense. If you have while(true){} then the loop cannot generate new mathematical constants… Thus it cannot be a source for new unique propositions that let you discriminate between before and after entering the loop? Or?

Sorry, I don't understand much of this.

Anyways, I don't have much more time to keep justifying my definition of assume. If you still don't like mine, maybe you can give your definition of assume, and demonstrate how that definition is more useful in the context of D.

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

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

I think that ship has sailed. 

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

> P.S. The current implementation also does not distinguish between a
> broken contract vs. a bug or problem encountered by the contract code.
> For example:

Last time I checked it also treated OOM and access violation (on windows) as contract failure too.  Any Throwable. 

"Sean Kelly"  wrote in message news:trnhymzwfkflgotxykmb@forum.dlang.org...

> Oh man, I forgot about this.  I wonder how this works from a codegen perspective.  Is precondition inheritance properly implemented yet?

Properly is a bit strong.  It is somewhat implemented.  I think there are still corner cases when some functions have no preconditions that people are still arguing over, but it does work for simple inheritance examples. 

On Fri, Aug 08, 2014 at 07:15:22PM +1000, Daniel Murphy via Digitalmars-d wrote:
> "H. S. Teoh via Digitalmars-d"  wrote in message news:mailman.684.1407434193.16021.digitalmars-d@puremagic.com...
> 
> >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,
> 
> I think that ship has sailed.

I know. It was more of a wish than anything.


T

-- 
Don't modify spaghetti code unless you can eat the consequences.

On Friday, 8 August 2014 at 14:27:56 UTC, H. S. Teoh via Digitalmars-d wrote:
> On Fri, Aug 08, 2014 at 07:15:22PM +1000, Daniel Murphy via Digitalmars-d wrote:
>> "H. S. Teoh via Digitalmars-d"  wrote in message
>> news:mailman.684.1407434193.16021.digitalmars-d@puremagic.com...
>> 
>> >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,
>> 
>> I think that ship has sailed.
>
> I know. It was more of a wish than anything.
>
>
> T

Since the ship HAS sailed... why must contracts be elided with --release? Seems to me if asserts go away, then eliding in and out is redundant. It'd be nice if I could put all my recoverable pre and post conditions inside those blocks as well. Just for organization's sake.

On Friday, 8 August 2014 at 18:43:22 UTC, Vlad Levenfeld wrote:
> Since the ship HAS sailed... why must contracts be elided with --release? Seems to me if asserts go away, then eliding in and out is redundant. It'd be nice if I could put all my recoverable pre and post conditions inside those blocks as well. Just for organization's sake.

An in or out block could have other code which is doing work in preparation for asserting rather than just assertions, so leaving them in wouldn't make sense.

- Jonathan M Davis