Исполнение при наличии привязок типов

Рассмотрим два определения функций

  test1 (x:nat) res:set of nat
    == { m | m:nat & m in set {0,...,x} };

  test2 (x:nat) res:set of nat
    == { m | m in set {0,...,x} & true };

Запуск test2(1000) в Overture дает набор натуральных чисел до 1000. Запуск test1(1000) дает набор натуральных чисел до 255. Я понимаю, что возникают сложности, когда в явных определениях функций есть явные привязки типов, но в в этом случае он просто молча дает неправильный ответ. Кажется, что когда в определении появляется привязка типа для натуральных чисел, диапазон ограничивается 0..255. По крайней мере, так кажется снаружи.

В главе 8 руководства по языку говорится: "Обратите внимание, что привязки типов могут выполняться интерпретаторами VDM только в том случае, если тип может быть определен статически конечным". Существуют ли правила, когда тип может быть выведен статически конечным?

Источник

2 ответа

Решение

Теперь я почти уверен, что такое поведение - особенность Overture, о которой я не знал. По умолчанию интерпретатор не может обрабатывать привязки типов для бесконечных типов, но на вкладке средства запуска "Отладчик" есть опция, позволяющая привязкам числовых типов (int, nat, nat1 и curiously, real) расширяться до диапазона целочисленных значений от "minint" в "maxint". Вы также должны поставить галочку в поле "numeric_type_bind_generation", чтобы включить эту функцию.

Поэтому я сожалею о ранней путанице. Я не думаю, что эта функция особенно полезна, и я никогда не слышал, чтобы кто-нибудь ее использовал, но я уверен, что она объясняет то, что вы видите.

Источник

Я не уверен, что здесь происходит для вас. Когда я пробую эту спецификацию с Overture 2.3.0 (а также с моментальным снимком 2.3.1 и VDMJ), функция test1 всегда завершается ошибкой, говоря:

Error 4: Cannot get bind values for type nat

Вы проводите этот тест как часть более широкой спецификации? Руководство правильное. Увертюра не может выполнить привязки типов, если она не может определить, что тип конечен, например, "bool", или что-то, состоящее полностью из конечных типов, например "set of bool" или "отображать P в Q", где P и Q конечны.

Основными конечными типами являются bool и все типы кавычек. Затем эти типы можно использовать для создания более сложных типов с помощью конструкторов типов - "множество из" и т. Д. Все конструкторы типов, кроме "seq of", будут давать конечный тип, пока все типы элементов являются конечными. Обратите внимание, что это включает [необязательные] типы, типы продуктов, такие как A*B, объединения типов, такие как A|B|C, и конструкторы записей.

Источник
Другие вопросы по тегам