c4j-team / c4j Goto Github PK
View Code? Open in Web Editor NEWContracts for Java
License: Eclipse Public License 1.0
Contracts for Java
License: Eclipse Public License 1.0
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.
E.g. on CloudBees.
...probably doesn't work.
Workarounds:
Not possible:
Preventing the need for the -javaagent and making it possible to ship signed archives with enabled contracts.
...instead of warning or whitelist-awareness (same with static fields?)
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.
C4J WARN - could not find a matching constructor in affected class external.Stack for the constructor defined in contract class external.StackContract
Using more than 255 local variables will lead to the compiler generating WIDE opcodes, which aren't handled correctly yet.
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)
On activation, a retransformation could be made, allowing the activation even if the classes were not transformed on class-loading.
As discussed with andrena board of directors and VKSI chair.
changesOnly prevents modifications on all fields of a class except for those specified.
For example, the following local configuration has no effect:
<configuration>
<root-package>singlepackage</root-package>
<pure-validate>true</pure-validate>
</configuration>
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.
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.
Jacoco-fields being instrumented by EclEmma are considered unpure, throwing AssertionErrors.
E.g. only pre-conditions, or pre-conditions + invariants, etc.
Will be discussed together with Jonas and Hagen in Stockholm.
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());
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:
@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.
...should only be evaluated in pre-condition, and only be retrieved from the OldCache in the post-condition.
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
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);
}
}
...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.
Discovered here: http://c2.com/cgi/wiki?TestWhetherInConstructionPhase
This allows a more generic approach to logging, leaving the decision, which logging framework to use, to the framework user.
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.
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.
This should give a significant performance improvement, e.g. when defining an equals-contract.
Given the following scenario
SuperClass
with external contract class SuperContractClass
and methode void method(int a)
TargetClass
, a sub class of SuperClass
, with external contract TargetContractClass
if (precondition())
block inside the definition of method method
of SuperContractClass
if (precondition())
inside the overrided method method
in TargetContractClass
<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
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>
Update description and links on http://www.andrena.de/know-how/c4j
It's a lot easier to extend with multiple projects.
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.