Run time checking with design by contract assertions

Hi,

I have downloaded a first version of IceCompiler, a small tool who allow
run time checks embedding in pharo classes on Smalltalkhub at

http://smalltalkhub.com/#!/~AlainRastoul/IceCompiler

If some interested pharoers are willing to give me feedback on this
package I would greatly appreciate.
This is not an announce but a request for feedback to advanced pharo
users , since it is an alpha version with probably killing side effects.
There is no ConfigurationOf as of today(there will be), but there is no
dependency and the package loads well in a fresh standard Pharo 5.0.


Checks are written in standard smalltalk methods with design-by-contract
style pragmas like

<contract: invariant>
<contract: #ensured appliedTo: #( #add: )>
<contract: #required appliedTo: #( #add: )>

Contract method calls are compiled in specified classes (with
subclasses) in order to make bullet-proofing run test phases of Pharo
code/image
  and to help in hard bug cases.


Before trying this package, please read the comments on smalltalk hub
page, because if misused it may break your image, and do not use on
standard important classes (Array, String, Dictionary, Collection etc.)
... unless you like danger :)


Many thanks in advance


regards,

Alain

This is cool. Having contract is really something I always wanted.

I do not know if Ice refers to Eiffel compiler mode but this is nice.

Le 25/2/16 23:48, Alain Rastoul a écrit :

Alain

can you give two example how to use the contract: ?

I would understand:

     <precondition: [can we pass a block here] >

Stef



Le 25/2/16 23:48, Alain Rastoul a écrit :

On 26/02/2016 10:16, stepharo wrote:
Hi Stef,

Yes this is completely inspired by Bertrand Meyer/Eiffel work.
I did an help page on that in the package info description on
smalltalkhub with more info, but here is an abstract:

precondition, postconditions, invariants are smalltalk checking methods
that returns true or false
and check that the object will perform/has performed (pre/post)  as
expected and is in a coherent state (invariants) .
This is not about program proof but run time checking.

I first tried with a block expressed as text in pragma as you suggest
(and as done in some frameworks with comments)
but it was difficult to use MetaLink with that, and MetaLink is a
powerfull tool I  wouldn't (and probably couldn't!) rewrite

Adding smalltalk methods is much more powerfull than simple text since
it integrates well with standard tools (debugger, browsers etc).
Those checks can be compiled in all the methods with the Icecompiler and
removed by recompiling the class with the standard compiler.

examples :

an invariant (a condition that is *allways* true) on a MyCollection
class would be expressed as a checkIndex method of class MyCollection

like:

checkIndex
        <contract: invariant>
        ^  firstIndex > 0
meaning : on every method call to  MyCollection, firstIndex *must* be > 0
if firstIndex goes <= 0 then the collection has a broken state
this will be checked before and after *every call* of *every method* of
MyCollection (except in the constructor an in other contract methods).


a pre condition to a call to add: method
preAdd: anObject
        <contract: #required appliedTo: #( #add: )>
        ^  anObject ~= self
meaning : you must not add a collection to itself
(note: this is just an example and I am not sure of that,
I think it does not make sense to add a collection to itself but may be
this is allowed?)
this will be checked before every call to MyCollection>>add:
(note2: appliedTo: allows to apply this check to several specific methods
- I didn't tested it yet but if it does not work then this is a bug)


a post condition that would be checked after every call:
postAdd: anObject
        <contract: #ensured appliedTo: #( #add: )>
        ^  self includes: anObject .
woudl check that after adding an object to a Mycollection, the
collection effectivly includes the object.
If it does not, this is reported as an error.

names (checkIndex, preAdd: , postAdd:) are not important, they are like
other methods of MyCollection.
The important thing is the 'appliedTo' part of the pragma who indicates
to which methods the contract applies.

Hi Alain,

Having contract is a valuable effort!

> On Feb 26, 2016, at 11:12 AM, Alain Rastoul <[hidden email]> wrote:
>
> <contract: #ensured appliedTo: #( #add: )>

What does that mean?
<contract: #ensured appliedTo: #( #add: )>

Alexandre

--
_,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:
Alexandre Bergel  http://www.bergel.eu
^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;.

On 26/02/2016 11:23, Nicolai Hess wrote:
> can you use symbols only for pragma arguments, please.
>
> <contract: #invariant>
> instead of
> <contract: invariant>
>
> I am about to change rbparser to only allow constant literal arguments
>
>
Yes, no problem
I noticed it worked but was not sure it was right
thank you for pointing that

On 26/02/2016 11:26, Alexandre Bergel wrote: Hi Alexandre,

a method with a pragma
<contract: #ensured appliedTo: #( #add: ) >
means it is a check that must be ensured by  (enforced by) the method to
which it applies (here add:).
The add: method of the object *must* verify this check, when the check
is executed, it must return true.

May be the terms I've choosed are confusing at first, but it was
voluntary, preCondition, postCondition are too much program execution
oriented IMHO, not enough assertive .

btw it is easy to change:
one could say here:
<contract: postcondition on: #( #add: )>

may be better ?

or may be better to support both ... :)


Alain

On 26/02/2016 11:50, Alain Rastoul wrote:
> one could say here:
> <contract: postcondition on: #( #add: )>

Correction,
after Nicolai's observation:
 > <contract: #postcondition on: #( #add: )>
(symbol)

--

Alain

On 26/02/2016 11:26, Alexandre Bergel wrote:
In fact I think may be better to use #before and #after since it is what
is used internally with MetaLink, it is clear and more developper
friendly, with singular and plural forms :

for contracts applied to only one method:
<contract: #before method: #add:>
<contract: #after method: #add:>


for contracts applied to several methods:
<contract: #before methods: #( #add: #addLast: #addIfNotPresent:)>
<contract: #after methods: #( #add: #addLast: #addIfNotPresent:)>


what do you think of that ?


--

Alain

I still do not understand. I would imagine something like:

foo
        <precondition: #invariant>
        <postcondition: #invariant>
        self bar


But, all in all, what are we using pragmas here?
I can always do:
        self assert: [ … ] description: …

Maybe we should specific a method called contractInvariant that is always executed before and after. Using Reflectivity.

Alexandre


--
_,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:
Alexandre Bergel  http://www.bergel.eu
^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;.

On 25-02-16 23:48, Alain Rastoul wrote:
> Hi,
>
> I have downloaded a first version of IceCompiler, a small tool who allow
> run time checks embedding in pharo classes on Smalltalkhub at

How does this compare to the earlier uContracts work by Angelo Lozano,
Kim Mens and Andy Kellens?

Stephan

On 26/02/2016 12:30, Alexandre Bergel wrote:
Assertions are used in standard java framework, but have hard side
effects : stopping the program immediately.
(cf
http://www.oracle.com/us/technologies/java/assertions-139853.html
"...The program will be aborted if the expression evaluates to false..")
With java it is possible, since the IDE and program are separated.

With Pharo you cannot, if you assert or throw an error in a sensible
place, you are likely to hang your image or to go for multiple errors
poping everywhere since you will break the state of an important object.


Another thing is that with dbc paradigm (assertions about your code),
there is no 'one invariant' but  lots of, you will not be able to
express them in a single method, even if you could it would be hundreds
lines and you would have to copy them in all methods you will want to check.
The complete horror to maintain when you change your code.


The use of pragmas make it possible to activate or deactivate those
contracts at compilation time, there will no overhead in standard
execution without contracts.
Think of the pragmas as a way to "inject" invariant compiled code into
the compiled method for testing, then you recompile without for release.

Adding invariants will have *big* performance impact, probably several
orders of magnitude, I'll measure.
The overhead will of course come from  calls of the checking framework,
but no doubt that with run-time reflexivity checking, you will have
something as sluggish too and you'll want to deactivate them  at compile
time ...

I'm ready to bet on that
one beer
  ... :)


--

Alain

On 26/02/2016 13:15, Stephan Eggermont wrote:

> How does this compare to the earlier uContracts work by Angelo Lozano,
> Kim Mens and Andy Kellens?
>
> Stephan
>
Well, I didn't know about that package, it looks good.

At least looking description on their web site, there is a cool
integration with Moose/Famix.
My package is at POC stage right now, probably far less elaborated
and more oriented towards runtime checking and debugging than contract
designing .

Very interesting, I'll digg into that.

Thank you for the pointer


--

Alain

Alexandre Bergel <[hidden email]> writes:

> I still do not understand. I would imagine something like:
>
> foo
> <precondition: #invariant>
> <postcondition: #invariant>
> self bar

I have the same feeling. It looks strange to me that the precondition
itself decides where it applies. I have the impression that each method
should list its preconditions.

--
Damien Cassou
http://damiencassou.seasidehosting.st

"Success is the ability to go from one failure to another without
losing enthusiasm." --Winston Churchill

Alexandre Bergel <[hidden email]> writes:

> But, all in all, what are we using pragmas here?
> I can always do:
> self assert: [ … ] description: …

you can do that for preconditions, but for postconditions it is harder
because there can be several exit points in a method.

--
Damien Cassou
http://damiencassou.seasidehosting.st

"Success is the ability to go from one failure to another without
losing enthusiasm." --Winston Churchill

> Assertions are used in standard java framework, but have hard side effects : stopping the program immediately.
> (cf
> http://www.oracle.com/us/technologies/java/assertions-139853.html
> "...The program will be aborted if the expression evaluates to false..")
> With java it is possible, since the IDE and program are separated.
>
> With Pharo you cannot, if you assert or throw an error in a sensible place, you are likely to hang your image or to go for multiple errors poping everywhere since you will break the state of an important object.

I do not think so. It is like putting a "self halt” (or “Halt now”). It is all done using exceptions.

> Another thing is that with dbc paradigm (assertions about your code), there is no 'one invariant' but  lots of, you will not be able to express them in a single method, even if you could it would be hundreds lines and you would have to copy them in all methods you will want to check.
> The complete horror to maintain when you change your code.

I would not be that pessimistic.

> The use of pragmas make it possible to activate or deactivate those contracts at compilation time, there will no overhead in standard execution without contracts.
> Think of the pragmas as a way to "inject" invariant compiled code into the compiled method for testing, then you recompile without for release.
>
> Adding invariants will have *big* performance impact, probably several orders of magnitude, I'll measure.
> The overhead will of course come from  calls of the checking framework, but no doubt that with run-time reflexivity checking, you will have something as sluggish too and you'll want to deactivate them  at compile time …

currently, the class Object define the method:
-=-=-=-=-=-=-=-=-=
Object>>assert: aBlock
        "Throw an assertion error if aBlock does not evaluates to true.
        We check for true explicitly to make the assertion fail for non booleans"
       
        aBlock value == true ifFalse: [AssertionFailure signal: 'Assertion failed’]
-=-=-=-=-=-=-=-=-=

It looks like a pretty convenient way to handle assertion. Nearly the same as in standard Java. Java offers the “assert” keywords, that you can disable by setting adequate option in the JVM.
If you want to disable the assertions in your class, you can simply redefine #asset: that does nothing.

Sure, you can imagine a solution using pragmas, but sincerely, I do not think it will be more flexible than using #assert:. Again, Java’s assertions are very similar to what we have now. However, I am pretty convinced there are great opportunities on writing assertions. It is really hard to write them, which is why not many are doing so.

Cheers,
Alexandre


> --
>
> Alain
>
>

--
_,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:
Alexandre Bergel  http://www.bergel.eu
^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;._,.;:~^~:;.

On 26/02/2016 16:37, Alexandre Bergel wrote:
...

>> With Pharo you cannot, if you assert or throw an error in a sensible place, you are likely to hang your image or to go for multiple errors poping everywhere since you will break the state of an important object.
>
> I do not think so. It is like putting a "self halt” (or “Halt now”). It is all done using exceptions.
>
Yes, that's the point: they are lots of places where you simply cannot
put self halt (timers, background processes - though in this case it
works... debugger magic :),  window resizing, mouse events )

>> Another thing is that with dbc paradigm (assertions about your code), there is no 'one invariant' but  lots of, you will not be able to express them in a single method, even if you could it would be hundreds lines and you would have to copy them in all methods you will want to check.
>> The complete horror to maintain when you change your code.
>
> I would not be that pessimistic.
>
Even if you write dedicated check methods to avoid pollute your  code,
you will have to call all the logic of your controls in each method, and
decide for each one what checks are applicable or not.
Thinking about object state checks (invariants), I cannot imagine I'll
have to add a: 'self checkThatxxx' in all the methods of my class...
...
>
> Sure, you can imagine a solution using pragmas, but sincerely, I do not think it will be more flexible than using #assert:. Again, Java’s assertions are very similar to what we have now. However, I am pretty convinced there are great opportunities on writing assertions. It is really hard to write them, which is why not many are doing so.

Thinking again about java asserts, they are more powerful framework who
do not use assert but comments which is like using pragmas.
http://www.javaworld.com/article/2074956/learn-java/icontract--design-by-contract-in-java.html
(they are plenty others, look at the end of
https://en.wikipedia.org/wiki/Design_by_contract in the language support)

In fact you are pointing to at the whole benefit of contracts when you
say that you can call assert or another method: of you own :
the good thing is that they are not linked to your code logic, they are
here to check things that you did not anticipate where they could
happen. You express what is correct for each method on entry, exit,
about the state of the object and the checks are injected into your code...
And you see this method that you would never have thought it could do
that in this improbable place ... :)

It is just a different way of checking that things are running ok under
the hood

Ah, and I am not against asserts or breakpoints, using contracts does
not forbid you to use assert:
  ... :)



--

Alain

On 26/02/2016 16:36, Damien Cassou wrote:
> Alexandre Bergel <[hidden email]> writes:
>
>> I still do not understand. I would imagine something like:
>>
>> foo
>> <precondition: #invariant>
>> <postcondition: #invariant>
>> self bar
>

Hi Damien,

Sorry for seeming pedantic but the concept is precise : when you express
an invariant it must be true for all code of your class.
(and they are several invariants for one class of course)

'Invariants' are conditions that do not change (hence the name)
they are about object state, they are not post or pre conditions they
are always true, in each methods, before and after
if you specify in which methods they are true, it means they could be
false in others and then they are not invariants by defintion ...

> I have the same feeling. It looks strange to me that the precondition
> itself decides where it applies. I have the impression that each method
> should list its preconditions.
>
That said, I think your example would be:
foo
        <precondition: myFooPrecondition>
        <postcondition: myFooPostcondition>

or something like:
foo
        <precondition: myFooPrecondition1, myFooPrecondition2 etc...>
        <postcondition: myFooPostcondition1, myFooPostcondition2 etc...>


you would say in each method what check applies.
That could be possible and the result would be the same

IMHO a bit less flexible, but another option.
Q: where would you define the invariants ?

a method that is never call and is tagged ?

myFooInvariant1
        <invariant>




--

Alain

On 25/02/2016 23:48, Alain Rastoul wrote:

@Stef, Alexandre, Damien, Nicolai, Stephan,

Thank you for the discussions, pointing me errors and interesting link.


I understood that the concept and/or it's implementation seems a bit
obscure, partly because of the syntax I've chosen for pragmas.


I will conform to some naming standards : #invariant/#pre/#post/on: will
be clearer than #required/#ensured/appliedTo:.

<contract: #invariant>
...
<contract: #pre on: #aMethod>
...
<contract: #pre on: #( #aMethod1 ... #aMethodn)>
...
idem post:
<contract: #post on: #aMethod>
...
<contract: #post on: #( #aMethod1 ... #aMethodn)>
...


I also note the suggestion of Damien (putting the pragma contracts in
the methods) but I am not truly convinced and it would imply some
rework, so I will not do that now - perhaps after a try.


examples

fooContract1
        <contract: #invariant>
        ^ myState notNil.

fooContract2
        <contract: #post on: #foo>
        ...

postAdd: anObject
        <contract: #post on: #(add: #addLast:)>
        ^ self includes: anObject

etc.





--

Alain