Лекция 2. Виды спецификаций поведения программных систем

виды спецификаций

виды связи между спецификациями и реализацией

прямая и обратная инженерия. ФМ в этих процессах

понятие метода разработки √ его отличие от языка спецификации

Практические цели курса (полученные навыки)

================================

QUEUE =
class

type Element,
Queue = Element-list

value empty : Queue,
put : Element >< Queue -> Queue,
get : Queue -~-> Queue >< Element

end

class

type Element,
Queue = Element-list

value empty : Queue,
put : Element >< Queue -> Queue,
get : Queue -~-> Queue >< Element

axiom forall e : Element, q : Queue empty is <..>,
get(put (e,q)) is (q, e)

end

class

type Element,
Queue = Element-list

value empty : Queue,
put : Element >< Queue -> Queue,
get : Queue -~-> Queue >< Element

axiom forall e : Element, q : Queue empty is <..>,

put (e,q) is q ^ <.e.>,
get(q) is (tl q, hd q)
pre q ~= empty

end

class

type Element,
Queue = Element-list

value empty : Queue,

put : Element >< Queue -> Queue
put (e, q1) as q2
post q1 ^ e = q2, // q2 - q1 ^e

get : Queue -~-> Queue >< Element
get (q1) as (q2, e)
post q2 ^e = q1 // q1 = q2 ^e
pre q ~= empty

end

прямая (forward engineering):
- требования, эскиз (проекта, реализации), уточнение, реализация, тесты
обратная (reverse engineering)
- legacy, спецификация модулей, восстановление архитектуры, тесты [, ре-дизайн]