-1

我将为这个场景简化一些事情（它在 Perfect Developer 中，它很快就会变得复杂）。假设我的类中有一个简单的模式，称为Succeed，它接受一个Course（这是一个先前定义的类）作为参数。

基本上，我想确保该课程set作为前提条件在我的课程中，然后将其添加到我coursesCompleted的后置条件中。这个简单的模式效果很好，看起来像这样：

schema !Succeed(c:Course)
pre
    c in allCourses
post
    coursesCompleted! = coursesCompleted.append(c);

但是，我想添加一个非常简单的if条件：如果我的 coursesCompleted 基数是 30 或更多，我想设置一个Diplomation枚举，比如说，“ Ok”。如果基数小于30，我将其设置为“ NotOk”

根据 Perfect Developer 的文档以及我见过的所有罕见示例，if语法应如下所示：

if [condition1] : do stuff;
   [condition2] : do other stuff;
fi

但是，如果我直接将其插入我的架构中，则如下所示：

schema !Succeed(c:Course)
pre
    c in allCourses
post
    coursesCompleted! = coursesCompleted.append(c),
    if [#coursesCompleted >= 30] : diplomation = Ok@DiplomationEnum;
       [#coursesCompleted < 30] : diplomation = NotOk@DiplomationEnum;
    fi

它不起作用，我总是以“非常具有描述性”结束

错误！关键字“if”的语法错误，应为以下之一：“！” '(' '?' 'c_address_of'

我已经尝试;在任何地方添加一些，在 之后添加一个via关键字post，更改它的位置，;与 s交易,，以及许多其他反复试验的东西。

所以我的问题是：如何if在 Perfect Developer 中向模式的后置条件添加条件？

请在 Perfect Developer 中回答。我（遗憾地）知道我的正式方法，我只需要if在世界上最糟糕的工具中编译。

4

1 回答 1

1

我可以使用 zet 表示法提供形式方法的解决方案，因为我没有使用 Perfect Developer，但是，该程序应该基于形式方法。据我所知，在正式方法中，如果系统在某些前提条件下具有不同的行为时不使用条件，而是创建具有不同前提条件的 2 个方法（我实现它的方式）或覆盖这两种场景的嵌套方法，用之间的逻辑或。当涉及到错误处理时，您首先提供一个最佳案例场景，然后定义一个健壮的方法定义（模式演算）。

在正式方法中，符号 ! 用于描述输出，而 ? 用于输入。

我希望这将帮助您了解可能的问题，因为它不是一个直接的完美开发者解决方案。但是，考虑到在形式方法中使用了数学这一事实，您可以使用以下规范并跳转到实现部分的任何程序/语言。

请注意：您将在以下模式中看到的关于先决条件/系统如何更改部分的任何内容都与逻辑 AND 相关联，但是我没有使用该符号，因为就不使用逻辑 OR 而言是隐含的。

所以这就是形式方法（Z-notation）中的样子。

在此处输入图像描述

于 2014-01-12T01:07:35.437 回答