k3
k3 copied to clipboard
Contracts (inv, pre, post) cannot be used in aspect classes
The @Contract + @Inv for design by contract with K3 cannot be used with the @Aspect annotations.
this simple example (on top of ecore )
package hello_ecore
import org.eclipse.emf.ecore.EPackage
import fr.inria.diverse.k3.al.annotationprocessor.Aspect
import static extension hello_ecore.EPackageAspect.*
import fr.inria.diverse.k3.al.annotationprocessor.Contracted
import fr.inria.diverse.k3.al.annotationprocessor.Inv
@Aspect(className=EPackage)
@Contracted
class EPackageAspect {
// @Inv def boolean noPackageInName(){
// return _self.name.nullOrEmpty || !_self.name.contains("Package")
// }
@Inv def boolean inv() { true }
}
raises the following error :
Invariant methods cannot declare any parameter
The same error occurs with pre and post conditions