Logica Hoare este un sistem formal cu un set de reguli logice pentru a raționa riguros despre corectitudinea programelor de calculator. Acesta a fost propus în 1969 de informaticianul și logicianul britanic Tony Hoare și ulterior rafinat de Hoare și alți cercetători.
Ce sunt triplele Hoare?
Un triplu Hoare are trei părți, o precondiție P, o instrucțiune de program sau o serie de instrucțiuni S și o postcondiție Q. De obicei este scris sub formă. {P} S {Q} Sensul este „dacă P este adevărat înainte ca S să fie executat și dacă execuția lui S se încheie, atunci Q este adevărată după”.
Pentru ce este folosită logica Hoare?
Scopul logicii Hoare este de a să ofere un sistem formal de raționament despre corectitudinea programului. Logica Hoare se bazează pe ideea unei specificații ca un contract între implementarea unei funcții și clienții acesteia. Specificația este alcătuită dintr-o precondiție și o postcondiție.
Ce este Hoare?
Hoare este un nume de familie englez derivat din engleza mijlocie hor(e) care înseamnă cărunt sau cu păr alb. Persoane notabile cu numele de familie includ: Albert Alfred Hoare, cunoscut sub numele de Bert Hoare (1874–1962), politician din Australia de Sud. Des Hoare (născut în 1934), jucător de cricket australian. … John Gurney Hoare (1810–1875), jucător de cricket englez și …
Este logica Hoare completă?
Răspunsul este da și arată că Logica Hoare este sunet. Soliditatea este importantă pentru că spunecă logica Hoare nu ne permite să derivăm afirmații de corectitudine parțială care de fapt nu sunt valabile. Dovada solidității necesită inducție asupra derivațiilor din ⊢ {P} c {Q} (omitem această demonstrație).
