How to insert a precondition into a method or constructor of a java class?

This is for the java class that I accept. The book mentions prerequisites and postconditions, but does not provide examples of how to encode them. It talks about claims, I have it, but the assignment that I perform specifically states to insert preconditions and check preconditions with statements.

Any help would be great.

+6
source share
5 answers

Languages ​​like the Eiffel support prerequisites and postconditions as the bulk of the language.

A convincing argument can be made that the whole purpose of the "constructor of objects" is precisely to establish the "class invariant".

But with Java (as with any other object-oriented post-C ++ language) you pretty much need to fake it.

Here's a great tech note about using Java "assert":

+3
source

Some examples given here express the preconditions as a parameter check and implement them in the statements. A non-private method should always perform parameter checking, as its caller goes beyond its implementation.

I tend to argue that parameter validation is not a prerequisite in the context of object-oriented systems - although I see many examples of such an approach in google.

My understanding of contracts began with [BINDER1999]; which defined the invariant, precondition and postconditions in terms of the state of the test object; expressed as Boolean predicates. In this appeal, we consider a method for controlling the state of a space covered by a class in which methods are transitions between states.

Discussion of preconditions and post-conditions in terms of parameters and return values ​​is much simpler than discussion in terms of state spaces! Therefore, I can understand why this view is much more common.

Recall that three types of contract are discussed:

  • an invariant is a test on an object-under-test that is true from the end of construction (any constructor), until it begins to be destroyed (although it can be broken during the transition).
  • Precondition - This is a test on an object-under-test, which must be true for the method-under-test, which must be called on the object-test.
  • A post-condition is a test on an object-under-test, which should be true immediately after the method completes.

If you take the (sensible) approach that overloaded methods should be semantically equivalent, then the prerequisites and post-conditions are the same for any overload of a given method in a class.

When considering interception and overridden methods, the contract project must follow the Liskov Substitution Principle; which leads to the following rules:

  • an invariant of a derived class is a logical AND of its local invariant and its base class.
  • The pre-condition of an overridden method is a logical-OR of its local precondition and the method in its base class.
  • The post-condition of the overridden method is logical-AND of its local post-state and method in its base class.

Remember, of course, that whenever a pre-condition or post-condition is checked, you must also check the invariant for the test class.

In Java, contracts can be written as protected Boolean predicates. For instance:

// class invariant predicate protected bool _invariant_ () { bool result = super._invariant_ (); // if derived bool local = ... // invariant condition within this implementation return result & local; } protected bool foo_pre_ () { bool result = super.foo_pre_ (); // if foo() overridden bool local = ... // pre-condition for foo() within this implementation return result || local; } protected bool foo_post_ () { bool result = super.foo_post_ (); // if foo() is overridden bool local = ... // post-condition for foo() with this implementation return result && local; } public Result foo (Parameters... p) { boolean success = false; assert (_invariant_ () && foo_pre_ ()); // pre-condition check under assertion try { Result result = foo_impl_ (p); // optionally wrap a private implementation function success = true; return result; } finally { // post-condition check on success, or pre-condition on exception assert (_invariant_ () && (success ? foo_post_ () : foo_pre_ ()); } } private Result foo_impl_ (Parameters... p) { ... // parameter validation as part of normal code } 

Do not collapse the invariant predicate into predicates of the pre- or post-state, as this will lead to the fact that the invariant will be called several times at each test point of the derived class.

This approach uses a wrapper for the sub-test method, the implementation of which is now in the private implementation method, and leaves the implementation body without the influence of contract statements. The wrapper also handles exceptional behavior - in this case, if you are throwing and throwing an exception, the precondition is checked again, as expected for a safe implementation.

Note that if in the above example, 'foo_impl_ ()' throws an exception and the subsequent statement of the precondition in the 'finally' block also fails, the original exception from 'foo_impl_ ()' will be lost in favor of the rejection of the statement.

Please note that the above is written off from the top of the head, so it may contain errors.

Link:

  • [BINDER1999] Binder, "Testing Object Oriented Systems," Addison-Wesley 1999.

Update 2014-05-19

I went back to the basics regarding entry and exit contracts.

The discussion above, and based on [BINDER1999], was considered by contracts in terms of the state-space of objects under test. Modeling classes as highly encapsulated state spaces is fundamental to building software in a scalable way - but that's another topic ...

Given how, when considering inheritance, the Lyskov Substitution Principle (LSP) 1 is applied (and required):

An overridden method in a derived class must be replaced for the same method in the base class.

To be replaceable, a method in a derived class should not be more restrictive in its input parameters than a method in a base class, otherwise it would fail if the base class method succeeded by breaking LSP 1 .

Similarly, the output values ​​and return type (where it is not part of the method signature) must be replaced for what is produced by the method in the base class - it must be at least restrictive in its output values, otherwise it will also violate LSP 1 . Please note that this also applies to the return type - from which rules about the types of returned sharing options can be derived.

Therefore, the contracts for the input and output values ​​of the overridden method follow the same rules for combination with inheritance and pre- and post-conditions, respectively; and for the effective implementation of these rules, they must be implemented separately from the method to which they are applied:

 protected bool foo_input_ (Parameters... p) { bool result = super.foo_input_ (p); // if foo() overridden bool local = ... // input-condition for foo() within this implementation return result || local; } protected bool foo_output_ (Return r, Parameters... p) { bool result = super.foo_output_ (r, p); // if foo() is overridden bool local = ... // output-condition for foo() with this implementation return result && local; } 

Please note that they are almost identical to foo_pre_() and foo_post_() respectively, and must be called in the test harness at the same test points as these contracts.

Preconditions and post-conditions are defined for the method family - the same conditions apply to all overloaded method variants. Input and output contracts apply to a specific method signature; however, in order to use them safely and predictably, we must understand the signing rules for our language and implementation (see C ++ using ).

Note that in the above example, I use the expression Parameters... p as a short for any set of parameter types and names; this does not mean that the variational method is implied!

+2
source

Just use assert to code the preconditions. For instance:

 ... private double n = 0; private double sum = 0; ... public double mean(){ assert n > 0; return sum/n; } ... 
0
source

A precondition is a condition that must be met at a given point during program execution, if program execution must continue correctly. For example, the statement "x = A [i];" has two premises: that A is not null and that 0 <= i <A.length. If one of these preconditions is violated, then executing the instruction will result in an error.

In addition, a prerequisite for a subprogram is a condition that must be true when the subprogram is called for the subprogram to work properly.

Here in detail and

Here is an example: preconditions-postconditions-invariants

0
source

To apply preconditions and postconditions in Java, you need to define and execute statements at runtime. In fact, this allows you to define runtime checks inside your code.

 public boolean isInEditMode() { ... } /** * Sets a new text. * Precondition: isEditMode() * Precondition: text != null * Postcondition: getText() == text * @param name */ public void setText(String text) { assert isInEditMode() : "Precondition: isInEditMode()"; assert text != null : "Precondition: text != null"; this.text = text; assert getText() == text : "Postcondition: getText() == text"; } /** * Delivers the text. * Precondition: isEditMode() * Postcondition: result != null * @return */ public String getText() { assert isInEditMode() : "Precondition: isInEditMode()"; String result = text; assert result != null : "Postcondition: result != null"; return result; } 

Please follow the above code here

0
source

All Articles