On Thu, 14 Apr 2011 17:12:53 +0200, Michal Kleczek <k...@g...com>
wrote:

>Anegdota:
>od razu zapuscilem gugla na "z language" i dostalem linki do wikipedii.
>Poniewaz jest to zwiazane z "formal methods" seria odnosnikow zaprowadzila
>mnie do http://en.wikipedia.org/wiki/B-Method - wymyslonej przez tegoz
>samego autora co Z. Tam przeczytalem ze:
>"B method has been used in some major safety-critical system applications in
>Europe (such as in Paris Métro Line 14 and Ariane 5 rocket)." - no, w koncu
>to metody formalne - do hardkorowych zastosowan.
>I natychmiast mi sie przypomnialo o wypadku
>http://en.wikipedia.org/wiki/Ariane_5_Flight_501
>spowodowanym przez blad w oprogramowaniu.
>
>Ehh... zycie jest okrutne.

Proponuje postudiowac DOKLADNIE przyczyny wypadku Ariane 5. Problem
polegal na tym ze do Ariane 5 zastosowano system nawigacyjny od Ariane
4 ktory byl zaprojektowany na mniejsze przyspieszenia niz Ariane 5
mogla osiagac podczas startu.

Trudno w tym przypadku obwiniac sofrwate - software zachowal sie
prawidlowo. Gdy liczby otrzymywane z systemu nawigacyjnego
przekroczyly dopuszczalny zakres, komputer wylaczyl system
nawigacyjny. Zgodnie ze specyfikacja.

Nie znam formalnych metod ktore sprawdzalyby poprawnosc i logike
zalozen projektowych.

A.L.