-
Notifications
You must be signed in to change notification settings - Fork 67
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
doc/manual: Add contract manual #2821
base: master
Are you sure you want to change the base?
Conversation
eb846e8
to
9a9d01d
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While I like the feature, I'm not a fan of the way it's documented here.
First, the information is weirdly scattered. I would merge all the Additional informations
directly where they belong. This is also important as people might read your documentation by jumping around the sections to find directly what they need.
Second, I would be wayyy more pedantic. Design by contracts is somehow not very popular today and not everyone know what you are talking about. This means explaining the why, the benefits and shortcomings of
this approach (or adding links to that), and also clearly picking the vocabulary you will be using and sticking to it.
Last, you don't showcase your feature enough. All the examples, while good, are super limited and don't give me much about the look and feel. Give me more examples of multiline-contracts? What about loops, how should I get around this? Can I add contracts to a constructor? Can I add a contract via redef
? One idea would be to use the part about inheritance to give a more involved and fully running example.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think someone without contract knowledge should read it.
for code block: do no fence AND indent
or else too much indentation
Also, check that your examples are functionnal with nitunit : it can run nit snipets in plain markdown as it was a big entity documentation.
doc/manual/contract.md
Outdated
|
||
## Writing invariants | ||
|
||
Invariants are used to specify the characteristics of a class/interface which must always be true, except when executing a member function. In other words, invariants define conditions that must be respected by our instance. Any instance which does not respect one or more of those conditions will be considered as incoherent. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
considered as incoherent weird grammar
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any instance which does not respect one or more of those conditions will be considered as in an incoherent state, and will cause an assertion failed.
Is it better like that?
doc/manual/contract.md
Outdated
end | ||
~~~ | ||
|
||
When a class defines an invariant all methods and constructors (inherited, redefined and introduced) will check this one. By default, the invariants are only checked on exit. See section `Verification policy` to activate them on in and out. For all constructors the invariant is only checked at the end of this, this is due to the fact that the object is not yet initialized. See the section `Execution order` for example. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe says that invariants are expensive because of that,
fbe395f
to
92a164a
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few typos and some minor changes but I really like this version!
doc/manual/contract.md
Outdated
Nit supports [contract programming](https://en.wikipedia.org/wiki/Design_by_contract). Contracts can be seen as the materialization of specifications in the code itself. The idea is to define the behavior of a property using conditions which will be evaluated on runtime. A contracts define the relations between a property and all its potential callers. If one of the two parties (callee/caller) does not respect the defined rules, the contract is considered to be broken and will cause a runtime error. | ||
|
||
You can put contracts on different elements of the language: methods, attributes, interfaces and classes in order to verify the conformity of the implementation compared with the specification. | ||
Different types of contracts exist. The preconditions (`expect`) and the postconditions (`ensure`) can be put on methods and attributes (setter) to define respectively the condition to check before and after the execution of the method. The invariants (`invariant`) that can be put on class and interface to define the conditions that must remain unchanged before and after the execution of each method of the class. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Different types of contracts exist. The preconditions (`expect`) and the postconditions (`ensure`) can be put on methods and attributes (setter) to define respectively the condition to check before and after the execution of the method. The invariants (`invariant`) that can be put on class and interface to define the conditions that must remain unchanged before and after the execution of each method of the class. | |
Different types of contracts exist: | |
* The preconditions (`expect`) and the postconditions (`ensure`) can be put on methods and attributes (setters) to define respectively the conditions to check before and after the execution of the method; | |
* The invariants (`invariant`) that can be put on classes and interfaces to define the assertions that must remain true before and after the execution of each method they contain. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"Unchanged conditions" sounded weird.
* `invariant` which designates the class invariants | ||
* `expect` which designates the preconditions | ||
* `ensure` which designates the postconditions. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Trop de which
|
||
## Writing invariants | ||
|
||
Invariants are used to specify the characteristics of a class/interface which must always be true, except when executing a member function. In other words, invariants define conditions that must be respected by our instance. Any instance which does not respect one or more of those conditions will be considered as in an incoherent state, and will cause an "assertion failed" error at runtime. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
J'écrirai plutôt cette section comme ceci:
Class invariants are conditions that must be held by its instances during runtime. These conditions allow you to limit the range of values allowed by an instance state at any given time. An assertion error will be raised if one condition is false.
3753cd0
to
9eb91cc
Compare
Signed-off-by: Florian Deljarry <[email protected]>
Test Results 66 files 314 suites 17m 14s ⏱️ For more details on these failures, see this check. Results for commit 68a1700. |
Here is the documentation for contracts. This is a little ahead of the current state of contracts.