Interface implementation with different types of termination measures

[gottschali]

Gobra verifies the following programs.
The interface I specifies a constant termination measure while the implementation uses a predicate termination measure.

package issue

type I interface {
	pred Mem()

	requires Mem()
	decreases 0
	m()
}

type S struct{}

pred (s *S) Mem() {
	true
}

requires s.Mem()
decreases s.Mem()
func (s *S) m() {}

(*S) implements I

The opposite case is also accepted where the interface specifies a predicate termination measure while the implementation uses a constant termination measure.

The same applies to other types of termination measures such as booleans, permissions, or tuple termination measures.

package issue

type I interface {
	pred Mem()

	requires Mem()
	decreases 1
	m(b bool, ghost p perm)
}

type S struct{}

pred (s *S) Mem() {
	true
}

requires s.Mem()
decreases p, b, s.Mem()
func (s *S) m(b bool, ghost p perm) {}

(*S) implements I

tested with Gobra d2bc4f8