why are languages like this one (Lustre) used for critical control software.
Perché alcuni strumenti software (o anche una metodologia) possono aiutare a parzialmente a dimostrare la correttezza del codice w.r.t. alcune specifiche formalizzate e perché alcuni altri strumenti software (o lo stesso, ad esempio SCADE) possono generare un codice C (che sarebbe "più sicuro" e forse più veloce di quanto il codice scritto a mano realisticamente raggiungere) dalla sorgente di Lustre.
Leggi informazioni su analisi del programma di origine statica .
Si noti che alcuni strumenti esistono per aiutare a dimostrare che alcuni programmi C (con uno stile di codifica limitato) sono in qualche modo "sicuri" o "corretti" w.r.t. alcune specifiche formalizzate ; per esempio. guarda Frama-C .
Inoltre, ricorda che alcuni sottoinsiemi dei linguaggi di programmazione (ad es. la maggior parte di Ocaml, grazie ad esso digita sistema , ma senza il suo infame Obj.magic trucco ) può "garantire" in base alla progettazione che il tuo programma ha vinto 'crash (per alcune ipotesi).
Ma ricorda: c'è No Bullet d'argento : a causa della indecidibilità del Halting Problem , non puoi sperare di provare completamente alcun software (e non puoi sperare di formalizzare interamente le sue specifiche e il suo ambiente, devi accettare che il software sia astrazioni ...)
Leggi anche il blog di Lattner: Cosa dovrebbe ogni programmatore C conoscere il comportamento non definito
A proposito, molte industrie (compresi i velivoli nucleari, gli aeromobili e persino i dispositivi sanitari ecc.) hanno le loro specifiche e normative relative al software critico di sicurezza. Ad esempio DO-178C per gli aeromobili commerciali. In questi casi, il software costa un lotto di più (ad esempio per riga di codice) rispetto alla normale applicazione telefonica e la metodologia di sviluppo del software è molto diversa (e molto più burocratica: documenterai e dovrai hanno formalmente accettato e testato qualsiasi cambiamento, anche una patch a linea singola).