Специализация в области анализа программ

Автор темы Андрей Миронов 
03.09.2000 23:05
Андрей Миронов
Специализация в области анализа программ
Уважаемые студенты 1-2 курса!

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

Одной из таких областей является теория анализа корректности компьютерных программ.

Задача анализа корректности программы заключается в следующем.

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

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

Например, анализируемая программа - это реализация некоторого
алгоритма сортировки, а спецификация - это формула в языке первого порядка
от двух переменных, пробегающих все массивы натуральных чисел,
которая истинна на паре массивов тогда и только тогда когда второй
массив - это отсортированный первый.

Программа может представлять собой также описание функционирования
некоторого вычислительного устройства (например, перемножителя чисел
с плавающей точкой).

Задачи анализа программ представляют исключительную актуальность:
в тех условиях когда программы управляют такими объектами как
самолёты, атомные электростанции, и т.д. от надёжности этих программ
существенно зависит безопасность людей.
Известно, что многие катастрофы на технических объектах были вызваны
некачественным программным обеспечением.

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

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

К сожалению, пока на мехмате нет ни одного семинара, посвящённого
этому направлению.

Но принципиальных трудностей, препятствующих
созданию такого семинара уже в этом семестре, нет.

Он может быть организован уже в этом семестре, если
будет достаточное количество студентов мехмата,
желающих специализироваться в этом направлении.

Те из вас, кто заинтересован в специализации в этом направлении,
просьба писать мне по адресу mironov@unb.ca

Желаю успехов,
Андрей Миронов http://www.cs.unb.ca/profs/mironov

P.S. Более подробно узнать о некоторых подходах к анализу программ
можно из моей статьи по адресу

http://www.cs.unb.ca/profs/mironov/rus_ag.ps
18.01.2001 01:25
Йцукке
всё есть не помню точное название семин
всё есть
не помню точное название семинара - хотя сам его посещаю :-)
на кафедре МЛиТА ведёт Сухомлин В.А.
18.01.2001 02:00
А.М.
О математическом уровне Сухомлина, как и
О математическом уровне Сухомлина, как и о математическом уровне
всех остальных профессоров с программистских кафедр ВМК
(точнее, о полном его отсутствии) я прекрасно знаю.

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

О результатах напишите сюда.
19.01.2001 00:02
Йцукке
ну я ещё маленький и только учусь кстат
ну я ещё маленький и только учусь
кстати - вышлите плз точное условие - а то курсовую писать надо - а я всё в поисках...
зы: не мне вас наверное учить - но публичный стёб - низкое занятие
19.01.2001 01:36
А.М.
Основные понятия и примеры см. на сайте
Основные понятия и примеры см. на сайте http://case.ispras.ru/mmoas/
В следующем семестре будет продолжено чтение спецкурса
по методам анализа программ (http://sp.cmc.msu.ru/win/courses/mmoas/)
19.01.2001 18:07
А.М.
Я хотел бы прокомментировать фразу насчё
Я хотел бы прокомментировать фразу насчёт публичного стёба.

Во всех дискуссиях я стараюсь придерживаться соответствия
стиля обсуждения характеру обсуждаемого предмета.

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

И я считаю что если обсуждаются вещи, которые
лично у меня вызывают чувство глубокого омерзения
(такие например как чрезмерная самоуверенность
мехматовской "элиты" по поводу того, что всё на мехмате
отлично и ничего не надо менять - а если есть какие-то
учебно-научные проблемы, то в них по определению
виноваты только студенты, или такие например как
полная деградация программистской науки на мехмате и ВМК,
несмотря на то что именно программирование сейчас является
наиболее популярным видом деятельности выпускников мехмата и ВМК),
то будет просто нечестно придерживаться при обсуждении
этих вопросов такого же тона, которым обсуждаются
"непроблемные" вопросы. Помимо нечестности, это оказывает
и вредное воздействие на формирование личности студентов,
участвующих в данной дискуссии, т.к. по сути это
является "облагораживанием зла".

Одной из главных задач Университета является не только
формирование навыков научной деятельности, но и целостное
формирование личности у студента, всестороннее развитие
его чувственной сферы. Для полноценной социальной адаптации
человеку важно иметь не только хорошо развитое чувство
прекрасного, но и хорошо развитое чувство безобразного,
которое должно быть спаяно с чувством прекрасного так же как
белая и чёрная капельки в известной китайской диаграмме.
Своим участием в данном форуме я стараюсь всеми доступными
мне способами подчеркнуть, какие чувства, на мой взгляд, должно
испытывать при обсуждении тех или иных вопросов.

Но конечно если моя активность на этом форуме приводит
к негативным результатам типа немотивированных непристойностей
в лифтах со стороны студентов, то мне остается только сказать
так же как сказал когда-то Мартин Лютер - "не этому я учил".

19.01.2001 18:30
id
Вот уж кто передернул...
> лично у меня вызывают чувство глубокого омерзения
> (такие например как чрезмерная самоуверенность
> мехматовской "элиты" по поводу того, что всё на мехмате
> отлично и ничего не надо менять - а если есть какие-то
> учебно-научные проблемы, то в них по определению
> виноваты только студенты, или такие например как

Нельзя ли уточнить, КТО КОНКРЕТНО и когда говорил Вам, что ВСЕ отлично, что НИЧЕГО не надо менять и что в учебных проблемах виноваты СТУДЕНТЫ?
Извините, только зарегистрированные пользователи могут публиковать сообщения в этом форуме.

Кликните здесь, чтобы войти