Логика разделения

Логика разделения, сепарационная логика (англ. separation logic) в информатике — формальная система, предназначенная для верификации программ, содержащих изменяемые структуры данных и указатели, расширение логики Хоара. Разработана Джоном Рейнольдсом (англ. John C. Reynolds), Питером О’Хирном (англ. Peter O'Hearn), Самином Иштиаком (англ. Samin Ishtiaq) и Хонсёком Яном (англ. Hongseok Yang) на основе работ Рода Бёрстола (англ. Rod Burstall). Язык утверждений логики разделения является специальным случаем логики пучковых импликаций (англ. logic of bunched implications).

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

Источник: Википедия

а б в г д е ё ж з и й к л м н о п р с т у ф х ц ч ш щ э ю я