规格形式化问题

指从自然语言需求产出语义匹配的形式化规约过程中存在的缺口问题，形式化验证只保证代码满足规约，却不保证规约忠实于需求