| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 453 B |
|
Quelle tau_declaration.pvs Sprache: PVS |
|||||||||
|
tau_declaration % [ parameters ]
: THEORY BEGIN % ASSUMING % assuming declarations % ENDASSUMING tau_type: TYPE = [ pn: posnat -> {t: nat | 2 * t < pn}] n: VAR nat pn: VAR posnat nada: tau_type = LAMBDA pn: 0 mid: tau_type = LAMBDA pn: floor((pn - 1) / 2) byz: tau_type = LAMBDA pn: floor(pn/3) weber(n): tau_type = LAMBDA pn: IF floor(n/2) < pn AND pn <= n THEN pn - 1 - floor(n/2) ELSE 0 ENDIF END tau_declaration ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28