k3 icon indicating copy to clipboard operation
k3 copied to clipboard

Contracts (inv, pre, post) cannot be used in aspect classes

Open dvojtise opened this issue 8 years ago • 0 comments

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

dvojtise avatar Apr 29 '16 14:04 dvojtise