0

我定义了两种类型：

public string = seq1 of char;
public config = map string to bool;

我还定义了一个测试集：dcl subFeatures : set of string := {"test1", "test2", "test3"}。

我正在尝试通过以下方式生成一组有效配置：

{ elem | elem : config & dom elem = subFeatures and {true} subset rng elem }

当一个配置至少有一个真实的范围值时，它被称为“有效” 。

Overture 正在启动错误Error 4: Cannot get bind values for type config。经过调查，我发现默认情况下 Overture 无法处理无限类型的类型绑定，但事实并非如此，我正在限制地图域。

有更多经验的人可以检查我做错了什么吗？

4

2 回答 2

0

尽管您编写的内容是有效的 VDM++，但正如您所说，如果它是有限类型，解释器只能枚举类型绑定（即“elem : config”）。但是，解释器也无法确定您已将无限类型减少为有限数量的元素。所以这在运行时失败。

要让解释器工作，您需要对子功能使用集合绑定并为每个功能创建“elem |-> true”。

编辑：

经过一番深思熟虑和帮助后，我认为我们可以得出结论，这对于非类型绑定理解是不可能的，或者会非常复杂。我认为下面的功能将实现您所需要的功能：

PossibleMappings: set of seq1 of char * map seq1 of char to bool -> set of map seq1 of char to bool
PossibleMappings(s,m) ==
    if s = dom m
    then {m}
    else let e in set s be st e not in set dom m in
        dunion {PossibleMappings(s, m munion {e |-> true}),
                PossibleMappings(s, m munion {e |-> false})};

ValidMappings: set of seq1 of char -> set of map seq1 of char to bool
ValidMappings(s) ==
    { m | m in set PossibleMappings(s, {|->}) & true in set rng m };

例如：

> p ValidMappings({"a", "b"})
= {
{"a" |-> false, "b" |-> true},
{"a" |-> true, "b" |-> false},
{"a" |-> true, "b" |-> true}
}
Executed in 0.027 secs.
于 2017-02-06T09:14:54.820 回答
0

我的建议是你会写这样的东西：

{ elem |-> {b | b : bool} union {true} | elem in set {"test1", "test2", "test3"}}
于 2017-02-06T18:33:31.967 回答