Верификация - Теория вычислительных процессов
1. Без ветвлений:
A) mov di,1
Mov al, adg
Add di, ax
Mov al, buf1[di]
Mov ah, buf2[di]
Sbb al, ah
TRUE
B) mov dl, buf1[di]
Mov bl, buf2[di]
Mov buf1[di],bl
Mov buf2[di],dl
TRUE {dl=buf1[di] ,bl=buf2[di] ,buf1[di]=bl, buf2[di]=dl}
(buf1[di]= buf2[di]( buf2[di]= buf1[di])
TRUE {dl=buf1[di] , bl=buf2[di] , buf1[di]=bl}
(buf1[di]= buf2[di])( dl= buf1[di])
TRUE { dl=buf1[di] , bl=buf2[di]}
(bl= buf2[di])( dl= buf1[di])
TRUE { dl=buf1[di]}
(buf2[di]= buf2[di])( dl= buf1[di])
TRUE (buf2[di]= buf2[di])( buf1[di]= buf1[di])
TRUE TRUE
TRUE
TRUE TRUE
TRUE
2. С ветвлением:
A) cmp flagbuf1,1
Je FirstNum
Jne SecondNum
FirstNum:
Mov Sign1,1
...
Jmp EndPerev
SecondNum:
Mov Sign2,1
...
Jmp EndPerev
EndPerev:
...
Для доказательства того, что
(flagbuf1=1)(flagbuf1=0)
{ if flagbuf1=1 then Sign1:=1 else Sign2:=1}
(Sign1=1Sign2=1)
Необходимо доказать три условия истинности:
- 1) без побочных эффектов (flagbuf1=1) 2) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=1) {Sign1:=1} (Sign1=1Sign2=1) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=1) ( 1=1 Sign2=1)
True True
True
- 3) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=0) {Sign2:=1} (Sign1=1Sign2=1) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=0) (Sign1=1 1=1)
True True
True
B) mov di,2
Mov cl, adg
LViv:
Mov al, buf3[di]
Inc di
...
Loop LViv
В этом примере является инвариантом.
Для доказательства того, что
Покажем, что цикл всегда завершается, и продемонстрируем истинность следующих утверждений:
- 1. Инвариант цикла удовлетворяется при входе в цикл, т. е. предусловие включает в себя инвариант: 2. Если инвариант истинен перед вычислением предиката управляющим циклом, то он истинен после его вычисления:
Т. к. вычисление свободно от побочных эффектов, то входное условие на рушиться не может, следовательно, утверждение истинно.
3. Инвариант цикла удовлетворяется в теле цикла:
True
4. Инвариант цикла и отрицание условия выполнения имплицируют постусловие:
True
Похожие статьи
-
СЕТЬ ПЕТРИ, ТЕКСТ ПРОГРАММЫ - Теория вычислительных процессов
Начальная разметка сети: одна фишка в позиции S1. После завершения функционирования сети фишка будет в позиции S2 Расшифровка переходов: 1. T1 - push f...
-
Назначение вычислительного кластера - Администрирование параллельных процессов
Кластеры используются в вычислительных целях, в частности в научных исследованиях. Для вычислительных кластеров существенными показателями являются...
-
Сетевыми протоколами называют протоколы первого и второго уровней, определяющих архитектуру локальной сети, в том числе ее топологию, передающую среду,...
-
Модель вычислительного процесса в GridMD - Повышение производительности работы библиотеки GridMD
Узлы графа исполнения, используемого в GridMD, представляют собой конкретные этапы исполнения, с которыми связываются действия, определяемые программным...
-
В работе использовались следующее программное обеспечение для решения поставленных задач: AutoCAD, ANSYS Workbench, ANSYS Icepak. Система AutoCAD...
-
Конечно-элементный анализ широко применяется при решении задач механики деформируемого твердого тела, теплообмена, гидро - и газодинамики, электро - и...
-
Вычислительные эксперименты для оценки эффективности параллельного варианта метода Гаусса для решения систем линейных уравнений проводились при следующих...
-
ВВЕДЕНИЕ, АНАЛИЗ ЗАДАЧИ - Теория вычислительных процессов
Ассемблер программа верификация Написать на языке ассемблер программу, реализующую вычитание двух целых упакованных 128- разрядных чисел. Описать...
-
Строгое определение протокола выглядит как формализованный набор правил, используемый ПК для коммуникаций. Из-за сложности коммуникаций между системами и...
-
СЕМАНТИКА, Схема подпрограммы вычитания - Теория вычислительных процессов
Операционная семантика команды sub al, 1 L1(al) 1 1 0 1 1 0 0 1 # 0 1 1 0 1 1 0 0 # L2 1. q01X1 Top1 q11 2. q11X1B1q02 3. q02X2 Top2 q12 4. q12X2 02 q22...
-
Объектом исследования является микросхема 4-х процессорной "системы на кристалле" на базе ядер 32-разрядных процессов цифровой обработки сигналов с...
-
Пересмотр теорий высказываний - Система отслеживания истинности предположений
Систему отслеживания истинности предположений, разработанную Мак-Аллестером [McAllester, 1980], нельзя отнести к самым первым, но ее, пожалуй, лучше...
-
ВВЕДЕНИЕ - Администрирование параллельных процессов
Последние годы во всем мире происходит бурное внедрение вычислительных кластеров - локальных сетей, с узлами из рабочих станций или персональных...
-
Коммуникационная библиотека PVM - Администрирование параллельных процессов
PVM (Parallel Virtual Machine) является продуктом исследовательского проекта по сетевым вычислениям в гетерогенной сетевой среде. Общая цель этого...
-
Цели создания проекта - Администрирование параллельных процессов
Создание кластера для организации параллельных вычислений связано с развитием и внедрением таких суперсистем, использование которых позволит упростить...
-
Моделирования случайных процессов - Теоретические основы информационных технологий
Моделирование случайных процессов - мощнейшее направление в современном математическом моделировании. Событие называется случайным, если оно достоверно...
-
Распределение задач между процессами - Администрирование параллельных процессов
Распределение подзадач между процессорами является завершающим этапом разработки параллельного метода. Надо отметить, что управление распределением...
-
Масштабирование набора подзадач - Администрирование параллельных процессов
Масштабирование разработанной вычислительной схемы параллельных вычислений проводится в случае, если количество имеющихся подзадач отличается от числа...
-
Разделение вычислений на независимые части - Администрирование параллельных процессов
Выбор способа разделения вычислений на независимые части основывается на анализе вычислительной схемы решения исходной задачи. Требования, которым должен...
-
Моделирование параллельных программ Рассмотренная схема проектирования и реализации параллельных вычислений дает способ понимания параллельных алгоритмов...
-
Параллельная виртуальная машина кластера кафедры АИС - Администрирование параллельных процессов
Так как в основе кластера АИС лежит параллельная система Beowulf, в качестве основы его вычислительной среды используем коммуникационную библиотеку PVM...
-
Программное обеспечение кластера, Операционная система - Администрирование параллельных процессов
Операционная система При построении кластера для организации параллельных вычислений более рационально иcпользовать свободно распространяемую...
-
Языки и методы параллельного программирования - Администрирование параллельных процессов
Применение параллельных архитектур повышает производительность при решении задач, явно сводимых к обработке векторов. Автоматическое распараллеливание...
-
ЗАКЛЮЧЕНИЕ - Администрирование параллельных процессов
В данной дипломной работе были рассмотрены вопросы, касающиеся разработки кластера для организации параллельных вычислений, а так же администрирование...
-
Формы и характеристики параллелизма Параллелизм -- это возможность одновременного выполнения нескольких арифметико-логических или служебных операций. На...
-
Принцип реализации СЛАУ на кластере - Администрирование параллельных процессов
Метод Гаусса - широко известный прямой алгоритм решения систем линейных уравнений, для которых матрицы коэффициентов являются плотными. Если система...
-
Требования к программному обеспечению системы На сетевом оборудовании должна функционировать межсетевая операционная система, причем ее версия должна...
-
Управление человеческими ресурсами компании является ключевым процессом деятельности компании, который управляет подбором, взаимодействием всех...
-
Нормативные правовые акты федерального уровня - Основы теории информации
Конституция Российской Федерации Федеральные конституционные законы Российской Федерации Федеральные законы Российской Федерации Указы и распоряжения...
-
Известно, что схемы процессов являются основой для настройки процесса в информационных системах. Схемы процессов легли в основу настройки процесса...
-
Уровни программного обеспечения. - Основы теории информации
1. Базовый уровень - самый низкий уровень ПО представляет базовое ПО. Оно отвечает за взаимодействие с базовыми аппаратными средствами. Как правило,...
-
Автоматизированные информационные системы - Технологический процесс в электронной промышленности
Полностью Автоматизированная информационная система или АИС -- это совокупность различных программно-аппаратных средств, которые предназначены для...
-
Типовые технологические операции - Технологический процесс в электронной промышленности
Технологический процесс (ТП) (сокращенно тп) -- это упорядоченная последовательность взаимосвязанных действий, выполняющихся с момента возникновения...
-
Функции СУБД: 1. ведение БД: ввод, корректир, сортировка, обработка, поиск данных, обработка по запросу. 2. обеспечение безопасности и целостности данных...
-
Кодирование информации -- процесс преобразования сигнала из формы, удобной для непосредственного использования информации, в форму, удобную для передачи,...
-
Объектно-ориентированные СУБД Несмотря на большую популярность реляционных СУБД, развитие технологии появления данными на них не остановилось. Развитие...
-
Процесс, Точность резки - Лазерная резка листового металла
Разрезание происходит с помощью воздействия на металлическое изделие лазерного луча. То есть, энергия луча вырезает отверстие в металле, расплавленный...
-
Управление процессом тесто приготовления может быть реализовано с помощью АСУТП (супервизорный режим) по модулю, который предусматривает два...
-
Для создания банка данных использовали пошаговый алгоритм, последовательно фотографируя картотеки встреч видов птиц с отметкой карточек, которые были...
-
На сегодняшний день уже практически невозможно представить нашу повседневную жизнь без компьютерной техники. Интернет предоставляет нам безграничные...
Верификация - Теория вычислительных процессов