pure functions and methods must have termination measures.
It seems inconsistent that this is not enforced for signatures in an interface definition.

type I interface {
	pure
	M() int
}

type T struct {}

pure
decreases
func (t *T) M() int {
	return 0
}

In a similar vein, Gobra accepts the following interface.
It cannot be implemented since pure methods must have exactly one out-parameter.

type J interface {
	pure
	M()
}