Указание ссылочной прозрачности в ACSL

Question

Я хочу найти аннотацию ACSL, которую можно применить к функции или указателю на функцию, чтобы указать, что она обладает свойством ссылочной прозрачности.Некоторый способ сказать, что «эта функция всегда будет возвращать одно и то же значение, если даны одинаковые аргументы».До сих пор я не нашел такой способ.Может кто-нибудь указать мне способ выразить это?

Может быть, какой-то способ обратиться к произвольной логической функции?Если бы я мог назвать неизвестное logic boolean uknown_function(void* a, void* b) = /* this is unkown */;, то я мог бы задокументировать функцию как имеющую постусловие, что она \result равна этой произвольной / неизвестной логической функции?

Больший контекст пытается выполнить стирание типасравнения.Я хочу в общих чертах выразить концепцию «пользователь дал мне void* s для работы и bool (*)(void const*, void const*) для их сравнения, и пользователь гарантирует мне, что предоставленная функция действительно является строгим частичным порядком по отношению к любойэти указатели указывают на ".Если бы у меня было это, то я мог бы начать описывать свойства сортируемых типов объектов, например, сортируемых.

Answer 1

В ACSL действительно нет прямой возможности сделать это: контракт функции определяет только то, что происходит во время одного вызова функции.Вы действительно могли бы полагаться на объявленную, но оставленную неопределенную логическую функцию, с предложением reads, которое определяет часть состояния памяти C, которая понадобится функции для вычисления ее результата, например,

/*@ logic boolean unknown_function{L}(int* a, int* b) reads a[0 .. 1], b[2 .. 3]; */

но если вы работаете с void *, не зная размера базовых объектов, это может быть сложно определить: если результат unknown_function не зависит исключительно от значения указателя, а не от содержимогоостроконечный объект, в этом случае вам не нужен этот reads трюк.

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

Наконец, вас может заинтересовать новый плагин RPP, который предлагает способ указания, подтверждения и использования свойств, связанных с несколькими вызовами одной или нескольких функций C (с).Он описан здесь и здесь , и публичное издание должно произойти в не столь отдаленном будущем.