Может ли условие OCL Post быть внутри оператора if then?

Я новичок в OCL и у меня есть некоторые сомнения относительно того, как работают предварительные и постусловия.

Можно ли поместить условие post в оператор if if?

Например, следующий фрагмент кода допустим или я просто смешиваю понятия?

Context [some context here]
if ( 
... some conditions...
) then ( 
result = 1
post: self.isComplete() -- for example
)
endif

Большое спасибо за Вашу помощь

Источник

3 ответа

Решение

Я бы переписал это как:

Context MyContext :: Integer
    post :
        if <some condition>
        then
            result = 1
        endif

Если вам нужно больше условий, вы можете сделать это с:

Context MyContext :: Integer
    post :
        if <some condition>
        then
            -- Another condition
            if self.isComplete()
            then
                result = 1
            else
               result = 0
            endif
        else
            result = 0
        endif
Источник

Вы можете использовать оператор подразумевает, как показано ниже:

context k 
inv
(k.count=0)implies(k.status='nothing')
Источник

Простой ответ. Нет. Объявление Complete OCL post: является независимым дополнением к операции.

Постусловие может не сработать, если фактические данные модели несовместимы с ожиданиями программиста OCL. Итак, если вы хотите провала, то вы попадаете в сложную область того, как OCL дает сбой надежно и с пользой. См. [1]. В качестве альтернативы, если вам просто нужен более сложный поток управления, перепишите, как указано в предыдущем ответе.

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

Предварительные и последующие условия плохо поддерживаются текущими инструментами. В USE есть возможность их выполнить, а в Eclipse OCL нет; они анализируются только для проверки синтаксиса. Выполнение пост-условий во время выполнения может быть очень дорогим и сложным, поскольку наиболее патологическое использование @pre может потребовать копии всего состояния системы.

Дорогостоящее выполнение во время выполнения может быть приемлемым для нескольких тестовых прогонов, но хотите ли вы причинить его своим конечным пользователям и что эти пользователи должны делать, если пост-условие не выполняется?

Работа, описанная в [1], использует символьный анализ для переноса оценки на время компиляции, гарантируя, что условия соблюдаются и не произойдет сбой во время выполнения, если будет использовано дополнительное время.

Однако никакой символьный анализ не может вместить все возможные потоки управления, поэтому необходима оболочка oclAssert(expr, invariant), чтобы помочь символьному анализу, утверждая, что локальный инвариант является истинным для возвращаемого expr. Аналогичная оболочка может поддерживать ваше использование, за исключением того, что вы хотите спровоцировать сбой во время выполнения, а не обещать, что опасность невозможна.

[1] http://www.eclipse.org/modeling/mdt/ocl/docs/publications/OCL2021Validity/OCLValidity.pdf

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