Un esecutore di specifiche logiche in tempo reale

Capitolo 1 Introduzione Come il linguaggio naturale traccia i confini della conoscenza comunicabile da uomo a uomo, cos` ı i linguaggi formali delimitano i possibili contenuti della comunicazione tra uomo e macchina. Solitamente, questa comunicazione ha come oggetto pi` u o meno esplicito un desiderio umano che la macchina dovr` a soddisfare. Nonostante essa sia sempre fedele nella sua esecuzione, non tutti i desideri si realizzano. Come in una famosa favola, il genio esegue alla lettera quanto richiesto e quando il risultato non ` e quello gradito, al protagonista non resta che prendersela con sestesso. A ben guardare egli potrebbe invocarenumeroseattenuanti, perch´ eper ogniformalismo esistono problemi abbastanza complessi da non ammettere soluzioni la cui formulazione sia di per s` e evidentemente corretta. La soglia di complessit` a sopra cui il semplice esame della soluzione non ` e sufficiente a determinarne la correttezza pu` o invece variare notevolmente con il livello del linguaggio in cui viene espressa. Tra i requisiti che ogni linguaggio formale dovrebbe soddisfare, i seguenti sono indici di un livello elevato: • Espressivit` a: deve essere possibile rappresentare i propri desideri • Precisione: i desideri devono essere rappresentabili senza ambiguit` a • Astrazione dal dettaglio: non deve essere necessario rappresentare dettagli ininfluenti • Compattezza: la rappresentazione deve essere ragionevolmente breve • Leggibilit` a: la rappresentazione deve essere comprensibile per altri lettori Un modo abbastanza naturale di conseguire il risultato desiderato ` e quello di impartire alla macchina una successione di comandi elementari riconosciuti che conduce all’obiettivo. Questa ` e l’essenza della programmazione imperativa ed i linguaggi formali attraverso cui si esprime, dal codice macchina a quelli ad oggetti, sono detti semplicemente “di programmazione”. Al crescere del loro livello si ` e per` o accompagnata una sempre maggiore rilevanza della sezione dichiarativa del programma, quella cio` e in cui si descrivono gli enti coinvolti nell’esecuzione, rispetto a quel- la imperativa. Nel frattempo, da istruzioni modellate sulla struttura dell’hardware ci si ` e pian piano elevati verso una sintassi che ricalca le forme del pensiero, come avviene nei linguaggi di programmazionelogicachesiispiranoalcalcolodeipredicatidelprimoordine. Questiultimisono particolarmente importanti perch´ e ` e possibile utilizzarli per scrivere programmi che ammettono una interpretazione completamente dichiarativa, cio` e che possono essere letti come la definizione di un insieme di relazioni priva di qualunque comando esplicito. I linguaggi di programmazione logica permettono quindi un diverso stile di scrittura, detto appunto dichiarativo, che conferisce al programma propriet` a rilevanti quali la possibilit` a di essere fuso con un diverso programma conservando la propria semantica. Parallelamenteailinguaggidiprogrammazionesisviluppavaunadiversacategoriadilinguaggi formali,detti“dispecifica”,ilcuiscopo` equellodiconsentireunadefinizionerigorosadell’obiettivo da raggiungere, a prescindere dalla strada che verr` a in effetti seguita. Le specifiche scritte facendo 1