RE: [eiffel_software] Re: void safety and dbc
- colin_paul_adams wrote:
> `is_my_attribute_attached, has no postcondition. ...Well, not quite. In the absence of an explicit postcondition, the postcondition is True. In any case, it can only be strengthened by a descendent toward False. So, the postcondition can be used and it should be made as strong as possible.
> A desecendant might redefine `is_my_attribute_attached'
> to return exactly the opposite result (or always False,
> or always True).
So, does the code compile if the code is:
__________Result := attached my_attribute
__________attached: Result = attached my_attribute
Peter Horan Faculty of Science and Technology
peter@... Deakin University
+61-3-5221 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA
+61-4-0831 2116 (Mobile)
-- The Eiffel guarantee: From specification to implementation
Important Notice: The contents of this email are intended solely for the named addressee and are confidential; any unauthorised use, reproduction or storage of the contents is expressly prohibited. If you have received this email in error, please delete it and any attachments immediately and advise the sender by return email or telephone.
Deakin University does not warrant that this email and any attachments are error or virus free.
- Hi Peter
Yes, in the case I had the first feature was detachable and that is a
source of confusion because it's a bad example. Recent posts by others
have actually done a better job of illustration. Neal's post of Aug 30
had a couple of good ones.
In reality, there are many cases where a feature's job is to assure the
programmer that a value is non-void and valid. Such features, it seems
to me have diminished importance if we then have to check voidness at
every turn. If we have checked validity, and it includes non-voidness,
and asserts that via postconditions, then _that_ check should suffice
instead of having to perform an explicit void check.
Even something as simple as
if is_valid_something (foo) then
Is no longer usable. Losing this kind of mechanism makes code less
readable and ultimately less good, defeating the goals of void safety
and DbC - and of Eiffel.
Roger F. Osmond
-------- Original Message --------
Subject: Re: [eiffel_software] void safety and dbc
From: Peter Gummer <p-gummer@...>
Date: Sat, September 01, 2012 3:32 am
> is_empty: BOOLEAN ...Hi Roger,
> void-safe-implication: not Result implies attached first ...
> The intent, regardless of the eventual syntax, is to exploit the
> specification aspects of contracts and make them partners with the more
> explict mechanisms of void safety. The result I think would be
> better-contracted and less defensive code.
I have a question, because I'm no closer to understanding what problem
you're trying to solve with your "implied non-voidness" proposal.
The postcondition above asserts that 'first' is attached when the
container is not empty. The fact that you need to assert this would
suggest that 'first' is declared detachable, right?
first: detachable FOO ... etc.
- Peter Gummer
- Hi Neal!
I just tried this in a junk project and the compiler does in fact now
see this CAP and reports no compile-time issues with the query feature:
> Unfortunately, (the last time I checked) the compiler does not (yet)realize that> > is_my_attribute_attached: BOOLEAN> do> Result :=
attached my_attribute> end
[Non-text portions of this message have been removed]
- --- In firstname.lastname@example.org, <rfo@...> wrote:
> Even something as simple asOne problem I see is that Void safety, as part of the type system, is currently designed to be thread safe while contracts, as run time checks, are not necessarily thread safe. Perhaps SCOOP will alleviate this mismatch.
> if is_valid_something (foo) then
> Is no longer usable. Losing this kind of mechanism makes code less
> readable and ultimately less good, defeating the goals of void safety
> and DbC - and of Eiffel.
Colin, good point about the post condition.