在Java中为接口添加不变量

Question

我一直在考虑创建一个允许程序员在接口上指定不变量(前置条件和后置条件)的Java框架.目的是使代码更加健壮,并减少需要为同一接口的不同实现编写的单元测试的数量.

我设想创建一些使用程序员也会编写的不变量来注释方法的方法.例如

interface Sort {
    int [] sort(int [] nums);
}

将使用注释进行修饰,以确保任何实现都返回已排序的列表.此注释将链接到可以在编译时针对任何实现运行的单元测试.

这是一个疯狂的想法还是对更广泛的编程社区有用？

Answer 1

这听起来可能与JML和ESC/Java有关，这两种技术在需要比通常的技术集提供的软件质量稍高一点的项目中得到了相当广泛的采用。