c# – 函数/方法的后置条件

发布时间：2020-12-14 19:13:59 所属栏目：Java 来源：网络整理

导读：有没有人记录过具有前后条件的函数或方法？ (我问,因为我的老师说这是正式/正确的方式)：传说:(因为我无法输入特殊字符) 3 将其读作“存在”和“存在” E 是(在集合中)的成员 A 为所有人暗示假设s是非空字符串.设B(s)是给出字符串s中位置索引的整数集. 这

有没有人记录过具有前后条件的函数或方法？ (我问,因为我的老师说这是正式/正确的方式)：

传说:(因为我无法输入特殊字符)
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是标准的数学符号,如果你完成了大学数学一年级课程,你会遇到它们. (可以说)有点不幸的是,人们使用的正式方法是善意或符号.它不必要地推迟/吓跑绝大多数(通常)对数学感到不舒服的程序员.

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!