Сегменты

Прежде чем продолжать уточнение и расширение SCHEDULE, необходимо обратиться к понятию SEGMENT. Можно начать со следующего описания:

indexing description: "Отдельные сегменты графика вещания" deferred class SEGMENT feature schedule: SCHEDULE is deferred end -- График, содержащий данный сегмент index: INTEGER is deferred end -- Положение сегмента в графике starting_time, ending_time: INTEGER is deferred end -- Время начала и завершения next: SEGMENT is deferred end -- Следующий сегмент, если он существует sponsor: COMPANY is deferred end -- Основной спонсор rating: INTEGER is deferred end -- Рейтинг сегмента (допустимость просмотра детьми и т.д.) ... Опущены команды change_next, set_sponsor, set_rating и др. ... Minimum_duration: INTEGER is 30 -- Минимальная длительность сегмента в секундах Maximum_interval: INTEGER is 2 -- Максимальная пауза между соседними сегментами в секундах invariant in_list: (1 "= index) and (index "= schedule.segments.count) in_schedule: schedule.segments.item (index) = Current next_in_list: (next /= Void) implies (schedule.segments.item (index + 1) = next) no_next_iff_last: (next = Void) = (index = schedule.segments.count) non_negative_rating: rating >= 0 positive_times: (starting_time > 0) and (ending_time " 0) sufficient_duration: ending_time - starting_time >= Minimum_duration decent_interval: (next.starting_time) - ending_time >= Maximum_interval end

Каждый сегмент "может определить" график, частью которого он является, и свое положение с помощью запросов schedule и index. Он содержит запросы starting_time и ending_time, к которым можно добавить и запрос duration, с инвариантом, связывающим длительность сегмента с временем начала и завершения. Такая избыточность допустима в системном анализе, добавление избыточных свойств отражает особенности, представляющие интерес для пользователей или разработчиков. Отношения между избыточными элементами фиксируются в соответствующих инвариантах. Инварианты in_list и in_schedule отражают позицию сегмента в списке сегментов и в графике.

Содержание Назад Вперед

Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий