📄 t15.use
字号:
-- $ProjectHeader: use 2-3-0-release.1 Mon, 12 Sep 2005 20:18:33 +0200 green $model t15 -- pre-/postconditionsclass Aoperations op1(p1 : Integer) : String post: 'AAA' <> 'BBB'endclass Battributes c : Integerendassociation R between A[*] B[1]endconstraintscontext a : A inv: a.b.c >= 0context A::op1(p1 : Integer) : String pre: p1.mod(2) = 0 pre: b.c > 0 post: b.c@pre = 0 post: self@pre.b.c = 0 post: Set{1,2,3}->notEmpty post: result = 'foo'context A::op1(p1 : Integer) : String post: true
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -