c4j-team / c4j Goto Github PK

Discovered here: http://c2.com/cgi/wiki?TestWhetherInConstructionPhase

...instead of warning or whitelist-awareness (same with static fields?)

optional: publish on any public repo

The only way this seems possible while keeping the ability to refactor is with an annotation on the static method, e.g.:

public class SomeClass {
  @StaticContractReference(StaticMethodContract.class)
  public static void staticMethod() {
    // ...
  }
}

public class StaticMethodContract {
  @StaticContract
  public void contractMethod() {
    if (preCondition()) {
      assert ...;
    }
    // ...
  }
}

This would not be possible when using external contracts, where a naming-convention is the only thing I can come up with. On the other hand, static methods should be rarely used. Maybe the Annotation-hassle isn't worth the effort at all.

As discussed with andrena board of directors and VKSI chair.

Up until now, constructor contracts were defined within the contract method's constructors themselves, matched by the signature of the constructor. This caused some problems, as there's always a default constructor available, and some of the initialization of the contract class is generated from the compiler.

Going forward, there has to be exactly one no-arg constructor in a contract class, which is solely responsible for initialization.

Contracts for constructors should be defined using the @ConstructorContract annotation on an arbitrarily named contract method. The signature is still responsible for matching the contract method and the actual target constructor.

The same should also apply for static initializers, using a static no-arg contract method with the @ConstructorContract annotation.

In cases where a post-condition is not called after the corresponding pre-condition was called, and the post-condition is using the unchanged()-mechanism, the Objects being stored in the PureEvaluator.unpureCache are not being cleaned up, causing a memory leak.

This probably also happens if the pre-condition throws an AssertionError. The only time the class-invariant is not executed is when the method itself throws a non-AssertionError.

To sum up, the behavior should be as follows:

• Pre-condition fails -> no further execution
• Method fails with AssertionError -> no further execution
• Method fails with non-AE -> execute Post-Condition
• Post-condition fails -> no further execution

C4J WARN - could not find a matching constructor in affected class external.Stack for the constructor defined in contract class external.StackContract

Unchanged and Pure doesn't work properly for:

param[0].setValue("abc");
param[0] = new SetLike();

See c4j-systemtest/de.andrena.c4j.systemtest.unchanged.UnchangedForObjectsSystemTest.

see http://maven.apache.org/guides/mini/guide-central-repository-upload.html

...when the value is actually being needed.

Sometimes, a value stored by old() is not actually being needed in the post-condition. It would be unnecessary to throw an exception if storing the value in the pre-condition threw the exception. We can therefore catch the exception and throw it only if the stored value is actually being retrieved in the post-condition.

According to the section Under the hood "C4J contains an instrumentor class that instruments all loaded classes that are protected by a contract class". But looking at the log I see that every class in the project is instrumented (even java.util and springframework).
Is this correct?

For example, you could configure a class ensuring that running the contracts takes at most 10% of the time it took running the actual methods of a class:

<class name="de.vksi.c4j.systemtest.config.contractoverhead.ContractOverheadSystemTest">
    <contract-overhead>10%</contract-overhead>
</class>

For example, the following local configuration has no effect:

    <configuration>
        <root-package>singlepackage</root-package>
        <pure-validate>true</pure-validate>
    </configuration>

Given the following scenario

1. Having a SuperClass with external contract class SuperContractClass and methode void method(int a)
2. TargetClass, a sub class of SuperClass, with external contract TargetContractClass
3. no if (precondition()) block inside the definition of method method of SuperContractClass
4. but a if (precondition()) inside the overrided method method in TargetContractClass
5. setting the configuration variable <default-precondition> to `undefined

` (or omitting it)

Expected behaviour: no "Found strengthening pre-condition" error

Observed behaviour: "Found strengthening pre-condition in method(int)" error is raised

...probably doesn't work.
Workarounds:

• call method using reflection
• ?

Not possible:

• making the target method public, would result in reflection change and possibly conflicts with other frameworks

@Contract should no longer need to load the contract-class and target-class, as this happens in the bootstrap class-loader when those classes may not be visible yet.

Jacoco-fields being instrumented by EclEmma are considered unpure, throwing AssertionErrors.

On activation, a retransformation could be made, allowing the activation even if the classes were not transformed on class-loading.

Will be discussed together with Jonas and Hagen in Stockholm.

This allows a more generic approach to logging, leaving the decision, which logging framework to use, to the framework user.

...should only be evaluated in pre-condition, and only be retrieved from the OldCache in the post-condition.

unchanged() and old() are only usable within contract methods themselves. As soon as a method is extracted containing unchanged() and old(), they no longer work.

C4J ERROR - Contract Violation in post-condition.
de.andrena.c4j.internal.ContractError: Contract Error in post-condition.
at de.andrena.c4j.internal.ContractErrorHandler.handleContractException(ContractErrorHandler.java:20)
at external.Stack.push(Stack.java:19)
at external.StackTest.isFullTestRight(StackTest.java:42)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
at org.junit.runners.BlockJUnit4ClassRunner.runNotIgnored(BlockJUnit4ClassRunner.java:79)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:71)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:49)
at org.junit.runners.ParentRunner$3.run(ParentRunner.java:193)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:52)
at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:191)
at org.junit.runners.ParentRunner.access$000(ParentRunner.java:42)
at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:184)
at org.junit.runners.ParentRunner.run(ParentRunner.java:236)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:50)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
Caused by: java.lang.ArrayIndexOutOfBoundsException: -1
at external.Stack.top(Stack.java:31)
at external.StackSpecContract.push(StackSpecContract.java:44)
... 27 more

Using more than 255 local variables will lead to the compiler generating WIDE opcodes, which aren't handled correctly yet.

changesOnly prevents modifications on all fields of a class except for those specified.

I want to use c4j in my eclipse based solution. But I only want to configure it in the Base Plugin once and use it in all dependant. How will it work without configure to c4j project in each Plugin?

This should be usable in a postcondition:

assert maxTime(2000); // this method must run within 2000 ms

Was already implemented in JoC with the @Profile annotation.

This should give a significant performance improvement, e.g. when defining an equals-contract.

This makes it possible to define so-called history properties of a class (as defined by Barbara Liskov). For example for a bounded Stack with a fixed capacity, the fact that the capacity may never be changed could be expressed with the folling statement in the class-invariant:

assert unchanged(target.capacity());

Just a thought: How about registering a custom domain for C4J? The website can be hosted on GitHub as well. In addition we could have nice email addresses and use it to name the Java packages accordingly.

Suggestion: c4j.org (if available)

E.g. only pre-conditions, or pre-conditions + invariants, etc.

E.g. on CloudBees.

E.g. enums use this to initialize their fields. This leads to illegal field access exceptions in pure validation, whenever an uninitialized enum is referenced within a pure context.

It's a lot easier to extend with multiple projects.

Preventing the need for the -javaagent and making it possible to ship signed archives with enabled contracts.

Example - assert getX() should really be assert target.getX():

public class A {

    private int x;

    public int getX() {
        return x;
    }

    public void setX(int x) {
        this.x = x;
    }

}

import static de.andrena.c4j.Condition.postCondition;
import static de.andrena.c4j.Condition.preCondition;
import de.andrena.c4j.Target;

public class AContract extends A {

    @Override
    public void setX(int x) {
        if (preCondition()) {
            assert x > 0 : "x > 0";
        }
        if (postCondition()) {
            assert getX() == x : "x set";
        }
    }

}

import org.junit.Test;

public class ATest {

    @Test
    public void test() {
        A a = new A();
        a.setX(5);
    }

}

Update description and links on http://www.andrena.de/know-how/c4j