OCL: Как я могу написать предварительные и постусловия для операции max, чтобы найти максимальное значение из коллекции?

Я пытаюсь написать предварительные и последующие условия, чтобы найти максимальное значение коллекции «col». Я не совсем уверен, как это сделать, рекурсивно, поэтому мне было интересно, может ли кто-нибудь помочь!

pre: true 
post: result = ...

uml preconditions ocl post-conditions
person mark    schedule 03.01.2013    source источник
comment
Возможно, вы захотите выразить это с помощью ограничения OCL — это однострочный   -  person    schedule 04.01.2013
comment
В таком случае... Как бы вы поступили? @Ластик? :)   -  person mark    schedule 04.01.2013

Ответы (4)


arrow_upward
3
arrow_downward

Что бы я сделал:

pre:  not col.isEmpty()
post: col -> includes(result) and col -> forAll(a | a <= result)

EDIT2: я обсуждал этот вопрос с некоторыми экспертами OCL. Они указали, что необходимо иметь col -> includes(result) в условии публикации. В противном случае result может быть любым значением, большим, чем все элементы col, но не обязательно является элементом col.

РЕДАКТИРОВАТЬ:

Постусловие означает: для каждого элемента a из col верно, что a <= result операция forAll определена на странице 45 Спецификация OCL 2.3.1. Его синтаксис

collection->forAll( v | boolean-expression-with-v )

Его семантика такова:

Выражение forAll возвращает логическое значение. Результат истинен, если логическое выражение истинно для всех элементов коллекции. Если логическое выражение-с-v ложно для одного или нескольких v в коллекции, то полное выражение оценивается как ложное. Например, в контексте компании:

Примеры:

 context Company
      inv: self.employee->forAll( age <= 65 )
      inv: self.employee->forAll( p | p.age <= 65 )
      inv: self.employee->forAll( p : Person | p.age <= 65 )
person gefei    schedule 04.01.2013
comment
Я не думаю, что этот ответ правильный, поскольку forAll возвращает логическое значение, а не элемент коллекции. - person Jordi Cabot; 04.01.2013
comment
@Jordi Я отредактировал свой ответ и вставил определение forAll из Спецификации. В моем пост-условии мне НЕ нужна эта функция для возврата элемента коллекции. - person gefei; 04.01.2013
comment
Я все еще не понимаю твоего решения. Ваше постусловие истинно для любого значения результата (хотя я не уверен, что вы можете использовать результат так же, как вы), больше, чем элементы коллекции, не обязательно максимальное значение - person Jordi Cabot; 04.01.2013
comment
если для каждого a в col, a <= result, то result является максимальным значением - person gefei; 04.01.2013

arrow_upward
3
arrow_downward

сообщение: результат = столбец -> любой (а | столбец-> для всех (а2 | а> = а2))

где «любой» возвращает один из элементов, удовлетворяющих условию, т.е. как выбор, но гарантирует, что возвращается только один элемент, выбранный случайным образом, если несколько элементов в коллекции удовлетворяют условию;

условие внутри «любого» гарантирует, что выбранный элемент «а» является максимальным значением в коллекции, сравнивая его со всеми остальными

Ознакомьтесь также с этим руководством по OCL . На самом деле ограничения OCL для работы с агрегатами и другими видами статистических функций являются одной из открытых проблем этого языка.

person Jordi Cabot    schedule 04.01.2013
comment
+1 за подробное описание запроса OCL и дополнительные ресурсы - person ; 04.01.2013
comment
@Jordi На самом деле этот ответ проблематичен. Просто предположим, что в коллекции есть два максимальных элемента e1 и e2, то есть предположим, что существуют e1 и e2, и она содержит col->forAll(e|e<=e1 and e<=e2), тогда в вашей формулировке есть проблема. - person gefei; 04.01.2013
comment
@gefei, вот почему я использую итератор any, а не select. Если есть несколько элементов с максимальным значением, любой возвращает один из них (случайным образом) - person Jordi Cabot; 04.01.2013
comment
@JordiCabot any возвращает либо e1, либо e2, вы не знаете. и результат тоже может быть либо e1 либо e2, тоже не скажешь. поэтому result = any(...) не обязательно верно. Напомним, что OCL является декларативным, а не императивным. - person gefei; 04.01.2013
comment
Я вижу, что мы не пришли к соглашению, так что пусть читатели решают сами. - person Jordi Cabot; 04.01.2013
comment
@JordiCabot Я думал об этом. Вы правы, ответ нормальный. Дело в том, что col->forAll(e|e<=e1 and e<=e2) подразумевает e1 <= e2 and e2 <= e1 и, следовательно, e1 == e2. Я пропустил это, когда писал комментарий выше. - person gefei; 05.01.2013

arrow_upward
1
arrow_downward

OCL определяет Collection::max() как

post: result = self->iterate( elem; acc : T = self.first() | acc.max(elem) )

где "операция max, поддерживаемая элементами, должна принимать один параметр типа T и быть одновременно ассоциативной и коммутативной".

Я понимаю, что это должно быть сообщение: result = self->itate( elem; acc : T = self.asSequence()->first() | acc.max(elem) ), потому что first() не определено для Collection.

Коллекция преобразуется в последовательность. Аккумулятор (acc) инициализируется первым значением последовательности. Выражение итерации обновляет аккумулятор как максимальное значение между текущим значением acc и итератором elem. Если коллекция пуста, результатом будет self.first(), то есть invalid.

person Javier    schedule 28.02.2013

arrow_upward
0
arrow_downward

Если я правильно вас понял, то, возможно, это может помочь: http://math.hws.edu/eck/cs124/javanotes6/c4/s6.html#subroutines.6.1

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

person Kamil    schedule 03.01.2013