Files
why3/bench/java/implements.mlw
2024-10-02 11:28:58 +02:00

20 lines
377 B
Plaintext

module AnInterface
[@java:package:fr.labri]
[@java:class_kind:interface]
type t
end
module AnImplementation
[@java:implements:fr.labri.AnInterface,java.lang.Comparable<AnImplementation>]
use AnInterface
use mach.java.lang.Integer
type t
let compare_to(self [@W:unused_variable:N]: t) (other [@W:unused_variable:N] : t) : integer = -1
end