if-statement - スキーマの事後条件に if ステートメントを追加するにはどうすればよいですか?

Question

このシナリオを単純化します (これは Perfect Developer にあり、すぐに複雑になります)。クラスに という単純なスキーマがあるとします。これは、(以前に定義されたクラス) をパラメーターとしてSucceed受け取ります。Course

基本的に、コースが前提条件として自分のコースにあることを確認してから、事後条件のセットにset追加します。coursesCompletedこの単純なスキーマはうまく機能し、次のようになります。

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

ただし、非常に単純なif条件を追加したいと思います。自分の courseCompleted カーディナリティが 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位置を変更したり、 と を交換したり;、,その他多くの試行錯誤を試みました。

私の質問は次のとおりです: ifPerfect Developer で、スキーマの事後条件に条件を追加するにはどうすればよいですか?

Perfect Developerでお答えください。私は（悲しいことに）自分の正式な方法を知っています。必要なのifは、世界で最悪のツールでコンパイルすることだけです。