Проверка программы на Python

Я преподаю курс по FOL и проверке программ, вдохновленный книгой Мордехай Бен-Ари, Математическая логика для компьютерных наук, Springer, 1993-2012. Я хотел бы проиллюстрировать понятия, запрограммировав студентов на Python.

Для FOL я использую NLTK, у которого отличный пакет FOL.

Но я еще не нашел пакета Python для проверки программы: вставки логических формул предусловия и постусловия, поиска инвариантов цикла, пошаговой проверки программы Python и т. Д. Другими словами, чтобы использовать Hoare логическая структура внутри Python и для программ Python.

Вы знаете какой-нибудь пакет для этой задачи?


python hoare-logic
person yannis    schedule 10.02.2014    source источник
comment
ммммм unittest + mock?   -  person Joran Beasley    schedule 10.02.2014
comment
FOL == Логика первого порядка?   -  person pillmuncher    schedule 10.02.2014
comment
Да, FOL = логика первого порядка, извините, что принял это как должное   -  person yannis    schedule 11.02.2014

Ответы (1)


arrow_upward
1
arrow_downward

Собираетесь преподавать MOOC по верификации программ? Или это будет обычный класс с экраном для отображения кода? Будет ли в вашем распоряжении белая доска?

Если вы хотите использовать дополнительные инструменты, тогда Online Python Tutor, разработанный профессором Филипом Гуо (http://www.pythontutor.com/) - отличный инструмент. Инструмент позволяет пошагово выполнять выполнение программы, показывая «состояние» программы (переменные и их конкретные значения). Насколько я знаю, он не позволяет напрямую указывать / выводить предварительные / пост-условия или инварианты цикла. Итак, я вижу случай, когда вы, как учитель, записываете на доске условия до и после публикации, шагаете по программе и объясняете классу, что условия действительно выполняются , показывая конкретные значения переменных с помощью наставника по Python. Практически аналогичный подход можно использовать для демонстрации инвариантов цикла.

Сказав это, pythontutor быстро становится популярным, и вопрос создателя о дополнительных функциях может помочь!

person Sudeep Juvekar    schedule 10.02.2014