Русские вычислители

Информация о пользователе

Привет, Гость! Войдите или зарегистрируйтесь.

Вы здесь » Русские вычислители » О языках программирования » Формализация языка C для HOL

Формализация языка C для HOL

Страница: 1
Ответить

Сообщений 1 страница 4 из 4

1

Британские учёные,

конкретно Michael Norrish. C formalised in HOL. University of Cambridge Computer Laboratory, 1998.
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf
HOL = Higher order logic (https://en.wikipedia.org/wiki/HOL_(proof_assistant))

20 лет как разрабатывают программы с доказуемыми характеристиками.
А в Кумире про такое и не слышали! (пруфлинк: http://ya.ru/?q=кумир+матлогика+pdf)

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

Тем временем в России утечки памяти ловят голыми руками.

За 20 лет, они ещё там дальше вперёд ушли, формализовывают не только ядра ОС, но и
компиляторы (CompCert):
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf
код файловых систем:
http://ssrg.nicta.com.au/publications/p … _RM_12.pdf
и СУБД:
http://ynot.cs.harvard.edu/papers/popl10.pdf

Нужно больше скелетов! http://e-collection.library.ethz.ch/ese … 601-02.pdf

Отредактировано ВежливыйЛис (23.07.2016 07:53:38)

0

2

Сделать семантические правила более наглядными идея хорошая. Но семантика это же домыслы! То что записано в коде это только часть тех правил которые применяет инженер при разработке.
Мы уже сразу теряем кучу информации. А поэтому доказать, что либо таким образом невозможно.
Любое дополнительное условие или правило вносит в процесс доказательство новые свойства. А они могут приводить к противоположным выводам.
Да и в нормальных книжках по испытаниям как раз об этом и говорится. Испытания должны строится так "чтобы они вместо поведения компилятора тестировали проведения кода."

Тем временем в России утечки памяти ловят голыми руками.

Не надо обобщать, своё не знание на всю Россию.

0

3

Павиа написал(а):

своё незнание

Ой-ой-ой...

Корпорация Microsoft использует автоматический доказатель теорем Z3 (MIT-лицензия) для верификации кода операционной системы Windows 7 и других программных продуктов (источник - https://ru.wikipedia.org/wiki/Автоматич … зательство )

The default Z3 bindings for .NET are built for the .NET framework version 4
https://github.com/Z3Prover/z3/tree/mas … api/dotnet

А в каких российских продуктах есть что-то лучше юнит-тестирования?

Отредактировано ВежливыйЛис (23.07.2016 17:26:55)

0

4

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

По поводу утечек памяти, так есть куча инструментов, вот далеко не полный список https://wiki.qt.io/Profiling_and_Memory_Checking_Tools
Заметь,там никаким HOL и не пахнет.

А в каких российских продуктах есть что-то лучше юнит-тестирования?

В каком плане лучше? Если говорить про автоматизацию, то это испытатели исходных текстов, такие как PVS-Studio. Они больше всего находят ошибок, без дополнительных телодвижений.

0

Ответить
Страница: 1

Быстрый ответ

Напишите ваше сообщение и нажмите «Отправить»


Вы здесь » Русские вычислители » О языках программирования » Формализация языка C для HOL