vdm++ - 通过 for all 循环运行集合时无法返回集合中的每个元素

Question

我试图通过 for all 循环运行包含 Brewage 对象的集合中的每个元素。但是当我尝试这样做时，返回值会变得混乱。

循环功能：

public pure Scan: set of Brewage ==> Brewage
Scan(brewage) == 
for all q in set brewage do 
return q

酿造构造：

public StringType = seq of char;
public StringLabel = seq of char;
public Char = char; 

instance variables
type : StringType;
label : StringLabel;
deposit : Char;

operations

public Brewage: StringType * StringLabel * Char  ==> Brewage
Brewage(ty, la, de) ==
(   type    := ty;
    label   := la;
    deposit := de
);

我得到的错误是在 Scan 函数中，如下所示：

操作返回 void 值。实际：(() | Brewage) 预期：Brewage

标签： vdm++vdm-sl

Answer 1

您可以使用 let 绑定来选择集合中的 Brewage，然后将其返回：

public pure Scan: set of Brewage ==> Brewage
Scan(brewage) == let b in set brewage in return b;

public main: ()==>Brewage
main()==
(
  let s = { new Brewage(), new Brewage() } in
    return Scan(s); 
);