W dniu 2015-03-28 10:54, M.M. pisze:

>> Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
>> (bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
>> inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
>> do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
> Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> wszystkie pary kodu, który może wykonać się równolegle, były
> opatrzone semaforami w tej samej kolejności w sensie wykonania i
> w odwrotnej kolejności (też w sensie wykonania).

Samo opatrzenie semaforami to często za mało by uniknąć dead-locka,
jeśli sekwencji chronionych jest więcej niż jedna. Dodatkowo dochodzi
jeszcze dbanie o integralność danych itp rzeczy.


--
Kaczus
http://kaczus.ppa.pl/art/liczbyzmiennoprzecinkowe,19
.html