有没有人记录过具有前后条件的函数或方法？ (我问,因为我的老师说这是正式/正确的方式)：
传说:(因为我无法输入特殊字符)
3 – 将其读作“存在”和“存在”
E – 是(在集合中)的成员
A – 为所有人
– > – 暗示
假设s是非空字符串.设B(s)是给出字符串s中位置索引的整数集.
这里开始记录这个函数：
int FirstOccurence(String s,Char c)
precondition:
(s.lenght() > 0) && 3 int i in B(s) [s.charAt(i) == c]
那是等待后置条件的前提条件;)
postcondition:
(FirstOccurence(s,c) E B(s)) && (s.charAt(FirstOccurence(s,c)) == c) &&
A int i B(s)[(i < FirstOccurence(s,c)) --> !(s.charAt(i) == c) ]
最佳答案
对.我遇到过它,虽然这在行业中并不常见.
在某些情况下,正确指定preconditions,postconditions和invariants绝对是最佳做法.例如：
>使用formal methods时;例如正式证明程序是正确的,或
>使用像Eiffel这样支持design by contract的编程语言时.
如果您想要一个关于Eiffel语言如何通过契约支持设计的示例,请查看here.
顺便说一下,“存在”的向后E和“为所有人”倒置的A是标准的数学符号,如果你完成了大学数学一年级课程,你会遇到它们. (可以说)有点不幸的是,人们使用的正式方法是善意或符号.它不必要地推迟/吓跑绝大多数(通常)对数学感到不舒服的程序员.
