Аналіз алгоритмів

[ правити ]=

} Разом з поширенням інформаційних технологій збільшився ризик програмних збоїв. Одним із способів уникнення помилок в алгоритмах та їх реалізаціях служать докази коректності систем математичними засобами.

Використання математичного апарату для аналізу алгоритмів і їх реалізацій називають формальними методами. Формальні методи передбачають застосування формальних специфікацій і, звичайно, набору інструментів для синтаксичного аналізу та докази властивостей специфікацій.Абстрагування від деталей реалізації дозволяє встановити властивості системи незалежно від її реалізації. Крім того, точність і однозначність математичних тверджень дозволяє уникнути багатозначності і неточності природних мов ^[15] .

За гіпотезою Річарда Мейса, «уникнути помилок краще усунення помилок»^[16] . За гіпотезою Хоара, «доказ програм вирішує проблему коректності, документації і сумісності» ^[17] . Доказ коректності програм дозволяє виявляти їх властивості по відношенню до всього діапазону вхідних даних.Для цього поняття коректності було розділено на два типи:

• Часткова коректність - програма дає правильний результат для тих випадків, коли вона завершується.

• Повна коректність - програма завершує роботу і видає правильний результат для всіх елементів з діапазону вхідних даних.

Під час докази коректності порівнюють текст програми зі специфікацією бажаного співвідношення вхідних-вихідних даних. Для доказів типу Хоара ця специфікація має вид тверджень, які називають передумовою та постусловіем. В сукупності з самою програмою, їх ще називають трійкою Хоара. Эти утверждения записывают

P { Q } R

где P — это предусловие, что должно выполняться перед запуском программы Q , а R — постусловие, правильное после завершения работы программы.

Формальные методы были успешно применены для широкого круга задач, в частности: разработке электронных схем, искусственного интеллекта, автоматических систем на железной дороге, верификациимикропроцессоров , спецификации стандартов и спецификации и верификации программ

Алгоритм пошуку рядка

Матеріал з Вікіпедії — вільної енциклопедії.

Неперевірена версія

Алгори́тими по́шуку рядка́ (англ. string searching algorithms) — важливий клас рядкових алгоритмів, що намагаються знайти місце де один або декілька текстових рядків (зразків, англ. pattern) входять у довший рядок або текст.

Зміст   [сховати]  1 Постановка задачі 1.1 Термінологія 1.1.1 Лема про суфікси, що перекриваються 2 Базова класифікація алгоритмів 2.1 Алгоритми пошуку для одного зразка 2.2 Алгоритми пошуку скінченної множини зразків 2.3 Алгоритми пошуку необмеженої множини зразків 3 Інші класифікації 3.1 Індексуючі методи 3.2 Інші варіанти 4 Джерела

[Ред.]Постановка задачі

Формальна постановка задачі пошуку рядка (англ. string-matching problem) така:

Нехай текст задано у вигляді масиву   довжини  , а зразок — масиву   довжини  . Передбачається, що елементи масивів — символи із скінченного алфавіту  . Наприклад, алфавіт може мати вигляд   чи  .

Зразок   зустрічається у тексті   зі зсувом   (англ. occurs with shift s), якщо   і   (іншими словами  ).

Якщо зразок   зустрічається у тексті   зі зсувом  , то величину  називають допустимим зсувом (англ. valid shift); інакше її називаютьнедопустимим зсувом (англ. invalid shift)

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