Формальне доведення правильності алгоритмів обробки дерев
Обмін місцями значень двох змінних. Звичайний цикл "поки" і команда повторення. Теорема про цикл, його інваріант і обмежуючу функцію. Програмування як цілеспрямована діяльність. Стратегія побудови команди вибору. Проектування та захисне програмування.
| Рубрика | Программирование, компьютеры и кибернетика |
| Вид | дипломная работа |
| Язык | украинский |
| Дата добавления | 15.06.2013 |
| Размер файла | 679,8 K |
Отправить свою хорошую работу в базу знаний просто. Используйте форму, расположенную ниже
Студенты, аспиранты, молодые ученые, использующие базу знаний в своей учебе и работе, будут вам очень благодарны.
Проектування за контрактом виходить з того, що «чим менше і конкретніше завдання, тим простіше розробка, підтримка і супровід коду». «З цієї глобальної точки зору простота стає критичним фактором. Складність - головний ворог якості ... Додаючи надлишкові перевірки, додаєте більше коду. Більше коду - більше складності, звідси і більше джерел умов, що призводять до того, що все піде не так. Це призведе до подальшого розростання коду, і так до нескінченності. Якщо піти по цій дорозі, то безперечно можна сказати одне - ми ніколи не досягнемо надійності. Чим більше пишемо, тим більше доведеться писати » [2].
Автор проектування за контрактом, Бертран Мейер вважає, що забезпечення надійності окремих модулів недостатньо для побудови надійного ПЗ. «Для систем як або істотних розмірів недостатньо забезпечення якості окремих елементів, - більш важливо гарантувати, що для кожного взаємодії двох елементів задано явний список взаємних зобов'язань і переваг - контракт».
ЧАСТИНА IІ.РОЗРОБКА ПРОГРАМ ТА ЇХ ДОВЕДЕННЯ У СИСТЕМІ FRAMA-C
2.1 Пошук елементу в масиві (саме праве входження)
2.1.1 Специфікація
Написати програму, яка у даному фіксованому масиві та при заданому значенні , знаходить саме праве входження значення змінної в масив . Якщо в масиві такого значення немає, повертає .
2.1.2 Ручне доведення
Запишемо передумову, післяумову, інваріант, обмежуючу функцію та тіло функції за допомогою мови предикатів та формальних означень циклу та розгалуження:
|
1.
За лемою отримаємо в нашому висловлюванні.
2.
Де
Доведемо обидві ці імплікації, виконавши відповідні підстановки:
3.
В лівій частині імплікації ми отримуємо протиріччя:
Це означає, що результат лівої частини , а результат всього виразу буде .
4.
5.
Oтримаємо наступне:
ВИСНОВКИ
Розглянуто теоретичні основи доведення правильності програм на основі найслабших передумов, зокрема:
- доведення розгалужень
- доведення циклів
- доведення присвоювань
- їх композицій довільної складності.
Опанована методика верифікації алгоритмів на основі найслабших передумов зокрема: визначення семантики мови програмування, підхід до доведення правильності послідовностей, підхід до доведення правильності розгалужень, підхід до доведення правильності циклів, стратегії побудови циклів та розгалужень.
СПИСОК ВИКОРИСТАНОЇ ЛІТЕРАТУРИ
1. Д. Грис. Наука программирования: Пер. с англ. - М.: Мир, 1984. - 416 с.
2. Т. Кормен. Алгоритмы. Построение и анализ. Русская редакция, 2005
3. Мейер Б. Объектно-ориентированное конструирование программных систем. М.: Русская редакция, 2005
4. C.A.R. Hoare. An Axiomatic Basis for Computer Programmimg. - Доступний з <http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf>.
5. ANSI/ISO C Specification Language- Доступний з < http://frama-c.com/download/acsl-implementation-Nitrogen-20111001.pdf>.
6. Ховард М., Лебланк Д. Защищенный код. 2-е издание. М.: Русская редакция, 2005
7. Макконнелл С. Совершенный код. 2-е издание. СПб.: Питер, 2005
Размещено на Allbest.ru
Подобные документы
Використання ітерацій для обчислення приблизних значень величин. Розробка ітераційних алгоритмів з перевіркою правильності введення даних. Побудова блок-схеми і програмування мовою Turbo Pascal обчислення значення функції, розкладеної в степеневий ряд.
лабораторная работа [197,2 K], добавлен 16.12.2010Методика та порядок програмування алгоритмів циклічної структури із заданим числом повторень за допомогою мови програмування VAB. Алгоритм роботи з одновимірними масивами. Програмування алгоритмів із структурою вкладених циклів, обробка матриць.
курсовая работа [27,7 K], добавлен 03.04.2009Мoвa прoгрaмувaння як систeма пoзначень, що служить для точного опису програм або алгоритмів для ЕOM. Вимоги до мов програмування, класифікація за їх особливостям. Загальна характеристика найбільш поширених мов програмування: Сі, Паскаль, Delphi, Бейсік.
реферат [24,4 K], добавлен 10.11.2012Розробка програмного додатку - гри "Jump way", яка поєднала в собі сучасні методи побудови 2D ігор. Обґрунтування вибору мови програмування. Проектування UML-діаграм класів. Користувацький інтерфейс. Програмна реалізація гри. Інструкція користувача.
курсовая работа [1,2 M], добавлен 09.01.2017Аналіз розроблення та програмування обчислювального процесу лінійної структури, налагодження програм. Вивчення правил запису констант, числових і символьних змінних, типів даних. Побудова алгоритму розв’язування завдання та креслення його блок-схеми.
реферат [2,1 M], добавлен 22.04.2012Модель аналізу-синтезу компіляції. Формальний опис вхідної мови програмування. Вибір технології програмування, проектування таблиць транслятора та вибір структур даних. Опис програми реалізації лексичного аналізатора. Розробка дерев граматичного розбору.
курсовая работа [75,8 K], добавлен 26.12.2009Розробка програми на мові програмування Асемблер для обчислення виразу. Розрахунок значень А, В, С у процедурах. Аналіз отриманих результатів за допомогою відлагоджувальника Turbo Debugger при різних заданих значеннях та перевірка їх правильності.
лабораторная работа [203,4 K], добавлен 09.01.2013Проектування і програмування обробки деталей на верстатах з числовим програмним управлінням. Проектування технологічної оперції обробки заготовки: вибір інструменту, ескізи наладок. Керуюча програма обробки деталей "кришка" та "вал". Верифікація програми.
курсовая работа [1,7 M], добавлен 29.11.2011Прототип об'єктно-орієнтованого програмування. Управління процесом реалізації програми. Розвиток апаратних засобів. Об'єктно-орієнтовані мови програмування. Надійність і експлуатаційні якості програм. Візуальне об’єктна-орієнтовне проектування Delphi.
контрольная работа [28,9 K], добавлен 18.05.2009Аналіз предметної області та відомих реалізацій гри 2048. Універсальна мова моделювання UML в процесі проектування гри. Розробка алгоритмів функціонування модулів гри "2048". Оператори мови програмування Python. Особливості середовища Visual Studio.
курсовая работа [1,2 M], добавлен 17.02.2021
