Установить понимание в VDM++

Question

Я определил 2 типа:

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 запускает ошибку Ошибка 4: Невозможно получить значения привязки для типа config. После исследования я обнаружил, что Overture по умолчанию не может обрабатывать привязки типов для бесконечных типов, но это не так, я ограничиваю область карты.

Может кто-нибудь с большим опытом проверить, что я делаю не так?

Answer 1

Хотя то, что вы написали, является допустимым 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. 

Answer 2

Я предлагаю вам написать что-то вроде:

{ elem |-> {b | b : bool} union {true} | elem in set {"test1", "test2", "test3"}}