Редактирование: ВПнМ, 02 лекция (от 15 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 30: | Строка 30: | ||
У нас есть система, строим более простую модель, на ней проверяем свойства. Причин строить модели две: | У нас есть система, строим более простую модель, на ней проверяем свойства. Причин строить модели две: | ||
- | * Программа, написанная на инженерном ЯП, предназначена для того, чтобы данные обрабатывать | + | * Программа, написанная на инженерном ЯП, она предназначена для того, чтобы данные обрабатывать |
- | * Абстракция от лишних | + | * Абстракция от лишних осстояний |
- | Мы хотим уменьшить пространство состояний. Что же такое | + | Мы хотим уменьшить пространство состояний. Что же такое состояний программы? |
* Состояние программы --- какой оператор выполняется, что записано в память (не только переменные, но и любые ресурсы, с которыми работает программа). | * Состояние программы --- какой оператор выполняется, что записано в память (не только переменные, но и любые ресурсы, с которыми работает программа). | ||
Строка 40: | Строка 40: | ||
Есть три переменных и 7 операторов --- 7*2^96 состояния. | Есть три переменных и 7 операторов --- 7*2^96 состояния. | ||
- | При этом, не все эти состояния по ходу порграммы достижимы. Число достижимых | + | При этом, не все эти состояния по ходу порграммы достижимы. Число достижимых сост. меньше, чем потенциальных, и нужно понимать, что просто смотря, анализируя текст программы, мы не можем оценить достиж. сост, поскольку эта задача алгоритмически неразрешима. |
второе число --- 6 * 3 * 2^64 | второе число --- 6 * 3 * 2^64 | ||
- | Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и | + | Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и дост. состояний, оценка должна быть обоснованная. По этому поводу лектор просит до след. среды написать на адрес model-checking@cs.msu.su, ФИО и группу и попросить дать порграмму. Если есть старосты групп, лектор просит прислать список групп |
Прежде чем говорить о моделировании, нужно поговорить о модели программ. Если говорить о языке С, то в качестве примера рассмотрим программу, подсчитывающую количество строк. У этой программы может быть очень большое число состояний, посмотрим, как её можно упростить: | Прежде чем говорить о моделировании, нужно поговорить о модели программ. Если говорить о языке С, то в качестве примера рассмотрим программу, подсчитывающую количество строк. У этой программы может быть очень большое число состояний, посмотрим, как её можно упростить: |