Семантика динамических систем
Содержание (FireFox,Safari)

3. Семантика динамических систем

Чтобы использовать преимущества "формального" подхода, можно сразу представить схему взаимоотношений для далее рассматриваемых абстракций.

Часть технических систем, обладающих ещё и свойством динамичности, служит прототипами здесь рассматриваемых абстрактных динамических систем.

Наиболее подробно будут рассматриваться системы мгновенного действия, а И-СЛЕДУЕТ и ЛИБО-СЛЕДУЕТ системам посвящены отдельные статьи.

Однако, основное внимание будет сосредоточено на ещё более узком классе автоматов мгновенного действия, введение которых обусловлено необходимостью рассмотривать некие регулярные правила усложнения.

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

Приходится поэтому определять ещё более узкий класс корректных автоматов мгновенного действия для которых уже будут строго определены формулы и соответствующая им семантика.

А описание произвольных автоматов мгновенного действия будет называться просто записью.

Проверку, является ли рассматриваемый автомат в том числе корректным осуществляет алгоритм синтеза.

Соответственно, и поведение строго определяется только для корректного автомата.

Основной стадией при разработке сложной технической системы обычно является такое её усложнение, которое сохраняет все полезные наработки.

То есть, монотонно(!) сохраняет смыслы отдельных фрагментов - смысл фрагмента, находящегося в составе более простой системы должен совпадать совпадать с его смыслом и в том случае, когда он оказывается в составе более сложной, но также корректной системы.

Именно инвариант монотонно раширяющихся контектов, формализованный через характерные черты поведения, и выступает в качестве смысла фрагмента в расширяющемся знании о системе.

Но, посольку способов усложнения может быть несколько, то для каждого из них надо доказать сохранение указанных характерных черт поведения.

Отсюда следует основное содержение работы:

Гиптеза: здесь предлагается монотонность проверять через понятие согласованности, а не напрямую через сохранение характерных черт поведения потому, что так "легче" во многих смыслах, что далее может быть продемонстрировано.

Также эта гипотеза объясняет предполагаемую область применения развиваемого подхода - когда конструкцию человек почти контролирует, а поведение - уже с трудом, то есть - реальне программы .

Назад Вперёд
ru/en