ru.algorithms

 
 - RU.ALGORITHMS ----------------------------------------------------------------
 From : Boris Sivko                          2:452/26.14    12 Apr 2003  22:09:53
 To : Vitaly Lugovsky
 Subject : Доказательство правильности ПО
 -------------------------------------------------------------------------------- 
 

 
     Дело "Re: Доказательство правильности ПО" было в Четверг Апрель 10 2003
 04:48 и заведено оно от Vitaly Lugovsky к Boris Sivko, но мне кажется, что в нём
 не хватало нескольких строк:
 
  BS>>  Совершенно не то.
  BS>>  Есть эл. схема с контроллером, известно что она делает и что она на
  BS>> самом деле собрана и работает. Hужно взять прогу и проверить её на
  BS>> возможность опасных отказов.
  VL>  Программу или схему? Если схему - то были кой какие верификаторы,
  VL> искать по ссылкам с http://www.haskell.org/ (e.g. Xilinx Lava вроде бы
  VL>  с верификатором был). Если программу - то всё просто: понять, что она
  VL> должна делать, аннотировать соответствующим образом, и доказать
  VL> соответствие аннотациям.
 
   Вопрос за какое время и с каким качеством будет это выполнено. Хотелось бы с
 минимальными потерями и без изобретения велосипедов.
   И задача которую ты формулируешь не совсем правильно решается, т.к. при
 доказательстве идёт поиск ошибок и всех возможных вариантов при которых могут не
 выполнятся условия док-ва. Теряется смысл проделываемых действий.
 
  BS>> Автор уже исчез, есс-но для док-ва прогу он пост- и пред-
  BS>> условиями не обеспечил, не говоря уже о инвариантах циклов. Ещё хуже
  BS>> если практически не соблюдается модульный принцип построения ПО. Так
  BS>> вот: нужно данное ПО привести к такому виду алгоритма, чтобы было
  BS>> проще осуществлять док-во при известных условиях док-ва.
  VL>  Hе проще ли переписать с нуля?
 
   Может и проще, но постановку задачи выполняю не я. Тем более что схема ужЕ в
 эксплуатации.
 
      Счастливо, Vitaly. Вспоминай обо мне...
 ... I'll be back...
  * Origin: Вперёд, вперёд, тебя за гробом слава ждёт! (2:452/26.14)
 
 

Вернуться к списку тем, сортированных по: возрастание даты  уменьшение даты  тема  автор 

Тема:    Автор:    Дата:    Re: Доказательство правильности ПО   Vitaly Lugovsky   10 Apr 2003 04:48:10   Доказательство правильности ПО   Boris Sivko   12 Apr 2003 22:09:53   Доказательство правильности ПО   Ilya Malyarenko   13 Apr 2003 14:08:00