1

我正在尝试编写前置条件和后置条件来找到集合“col”的最大值。我不确定如何递归，所以我想知道是否有人可以提供帮助！

pre: true 
post: result = ...
4

4 回答 4

3

我会做什么：

pre:  not col.isEmpty()
post: col -> includes(result) and col -> forAll(a | a <= result)

EDIT2：我与一些 OCL 专家讨论了这个问题。他们指出有必要col -> includes(result)在后置条件下。否则result可能是大于 的所有元素的任何值col，但不一定是 的元素col。

编辑：

后置条件意味着：对于 的每个元素a，操作在OCL 规范 2.3.1的 第45 页上定义col是真的。它的语法是a <= resultforAll

collection->forAll( v | boolean-expression-with-v )

它的语义是：

这个 forAll 表达式产生一个布尔值。如果布尔表达式对集合的所有元素都为真，则结果为真。如果 boolean-expression-with-v 对于集合中的一个或多个 v 为 false，则完整表达式的计算结果为 false。例如，在公司的背景下：

例子：

 context Company
      inv: self.employee->forAll( age <= 65 )
      inv: self.employee->forAll( p | p.age <= 65 )
      inv: self.employee->forAll( p : Person | p.age <= 65 )
于 2013-01-04T08:41:40.983 回答
3

帖子：结果= col -> any(a | col->forAll(a2 | a >=a2))

其中“any”返回满足条件的元素之一，即类似于选择但保证仅返回单个元素，如果集合中的多个元素满足条件则随机选择；

"any" 中的条件通过与所有其他元素进行比较来保证所选元素 "a" 是集合中的最大值

另请查看此OCL 教程。事实上，OCL 在处理聚合和其他类型的统计函数方面的局限性是这种语言的开放问题之一。

于 2013-01-04T10:27:09.200 回答
1

OCL 定义Collection::max()为

post: result = self->iterate( elem; acc : T = self.first() | acc.max(elem) )

其中“元素支持的最大操作必须采用 T 类型的一个参数，并且是关联的和可交换的”。

我知道它应该是 post: result = self->iterate(elem; acc : T = self.asSequence()->first() | acc.max(elem) ) 因为first()没有为Collection.

该集合被转换为一个序列。累加器 ( acc) 用序列的第一个值初始化。迭代表达式将累加器更新为当前值acc和迭代器之间的最大值elem。如果集合为空，则结果为self.first()，即invalid。

于 2013-02-28T18:37:02.807 回答
0

如果我理解正确，那么这可能会有所帮助： http: //math.hws.edu/eck/cs124/javanotes6/c4/s6.html#subroutines.6.1

前提条件是在执行方法之前必须满足的条件。这主要是关于输入数据的一些断言，例如集合不为空。后置条件定义了方法完成后的真实情况。在您的情况下，这可以是例如：该方法返回的元素在给定集合中具有最大值。

于 2013-01-03T20:49:09.230 回答