caxapa.ru :: в режиме прохожего: система подвергается функциональной декомпозиции -> записывается на хаскеле. далее

TimeZoneDefault (12.02.2016 13:05, просмотров: 1) ответил Evgeny_CD на Д.ARMоед - подскажи, плиз....

в режиме прохожего: система подвергается функциональной декомпозиции -> записывается на хаскеле. далее существуют средства верификации для прог на хаскеле, напр. Programatica: programatica.cs.pdx.edu/P/ProgramaticaAssurance.pdf - Information provided by textbooks, component specifications, and other resources. - Individual test cases. - Random testing. - Formal proof. подозреваю, что пользовали именно древнюю программатику(не увидел в тексте), но в ней возможен прувер Isabelle(на него ссылаются). после исправлений прога транслируется с хаскеля на си. вроде так.

- Спасибо! Да, у них там есть хаскельный код в репозитории, и какой-то кодогенаратор на их собственном DSL. Все это весьма близко к подходам, которые я здесь много лет ковыряю. А именно - программист пишет не "сразу в С", а в некий DSL, который, в Evgeny_CD(147 знак., 12.02.2016 16:28)
  - последний тезис упирается в понятие "обратимых вычислений", которые существуют не для всех классов алгебр. для алгебры чёрча - формально не существуют :) TimeZoneDefault(801 знак., 12.02.2016 17:18, )
    - Спасибо! "частный случай полупрямого произведения групп." Да, это надо переварить.... - Evgeny_CD(12.02.2016 17:52)
      - переварить лучше то, что фичи, представляемые в виде "proved" решений для сегодняшних камней на самом деле таковыми не являются в силу фундаментальных причин. - TimeZoneDefault(12.02.2016 19:46, )
        
        "Не нее-шь, не продаш" :) - Evgeny_CD(12.02.2016 20:58)
        
        пральна. осталось понять, как нае..ть всех так, чтобы им это понравилось :)) - TimeZoneDefault(12.02.2016 21:39, )

Средства и методы разработки