Вопросы с тегом «formal-methods»

25
Существуют ли аннотированные системы формальной проверки для чисто функциональных языков программирования?

ACSL (Ansi C Specification Language) - это спецификация для кода C, снабженная специальными комментариями, которая позволяет формально проверять код C. Я не рассматривал это, но я полагаю, что формальные методы, используемые в верификаторах ACSL , будут похожи на Hoare Logic. Однако для чисто...

23
В какой степени алгоритм может предсказать сложность времени произвольной входной программы?

Проблема Halting гласит, что невозможно написать программу, которая может определить, останавливается ли другая программа, для всех возможных программ ввода . Тем не менее, я могу, конечно, написать программу, которая может вычислить время выполнения программы вроде: for(i=0; i<N; i++) { x = 1;...

22
Учебный план: логические / формальные методы в безопасности

В настоящее время я преподаю небольшой курс (четыре двухчасовых лекции на уровне магистратуры) по логическим методам в безопасности , хотя название « Формальные методы в безопасности» может быть более подходящим. В нем кратко рассматриваются следующие темы (с соответствующими логическими методами):...

20
Как мы можем знать, что формальные методы работают?

Важной целью формальных методов является доказательство правильности систем, либо автоматизированными, либо управляемыми человеком средствами. Тем не менее, кажется, что даже если вы можете предоставить подтверждение правильности, вы НЕ МОЖЕТЕ гарантировать, что система не выйдет из строя....

17
Указатели для CS приложений логики

Я аспирант по математике с твердым опытом в логике. Я прошел годичный курс для выпускников по логике вместе с курсами для выпускников по теории конечных моделей и другим курсам по принуждению и теории множеств. Большинство текстов CS, кажется, предполагают только очень скромный фон в логике,...

15
Как создать критически важное программное обеспечение?

Я самостоятельно изучаю формальные методы. Я слышал, что формальные методы используются (и обычно используются только) для создания критически важных программ (таких как контроллер ядерного реактора, контроллер полета самолета, контроллер космического зонда). Вот почему мне интересно узнать это: p...

9
Можно ли вычислить, равны ли две функции экстенсионально?

Если у вас есть две функции, реализующие другой алгоритм сортировки, то можно ли по исходному коду сделать вывод, что они имеют одинаковые внешние свойства? Это означает, что у них обоих будет возможная несортированная последовательность в качестве входных данных и отсортированная...