|
ru.algorithms
- RU.ALGORITHMS ----------------------------------------------------------------
From : Vitaly Lugovsky 2:5080/1003 10 Apr 2003 04:48:10
To : Boris Sivko
Subject : Re: Доказательство правильности ПО
--------------------------------------------------------------------------------
Boris Sivko <Boris.Sivko@p14.f26.n452.z2.fidonet.org> wrote:
> BS>> В тематике данной эхи интересует:
> BS>> - алгоритмизация уже существующего ПО для док-ва;
> VL> В смысле - написание спецификаций и/или аннотаций?
> VL> Это эквипенисуально собственно самим алгоритмам.
> BS>> Я уже не в первый раз сталкиваюсь с задачей, когда есть прога, а
> BS>> автора нет и нужно по поставленной задаче и условиям док-ва строить
> BS>> всё с нуля.
> VL> А... Догадаться по реализации, какой была постановка задачи?
>
> Совершенно не то.
> Есть эл. схема с контроллелом, известно что она делает и что она на самом
> деле собрана и работает. Hужно взять прогу и проверить её на возможность
> опасных отказов.
Программу или схему? Если схему - то были кой какие верификаторы,
искать по ссылкам с http://www.haskell.org/ (e.g. Xilinx Lava вроде бы
с верификатором был). Если программу - то всё просто: понять, что она
должна делать, аннотировать соответствующим образом, и доказать соответствие
аннотациям.
> Автор уже исчез, есс-но для док-ва прогу он пост- и пред-
> условиями не обеспечил, не говоря уже о инвариантах циклов. Ещё хуже если
> практически не соблюдается модульный принцип построения ПО. Так вот: нужно
> данное ПО привести к такому виду алгоритма, чтобы было проще осуществлять
> док-во при известных условиях док-ва.
Hе проще ли переписать с нуля?
--- ifmail v.2.15dev5
* Origin: (http://news.cca.usart.ru/) USURT's FidoNET<-> (2:5080/1003@fidonet)
Вернуться к списку тем, сортированных по: возрастание даты уменьшение даты тема автор
|
