Videocorso Ada CGFA
Il linguaggio dei sistemi dove un errore non è ammesso: aerei, treni, satelliti. Con GNAT e un'introduzione a SPARK
- Partenza: Da zero
- 14 ore con gli esercizi
- 10 lezioni in 3 livelli
- 2 lezioni gratis
Video in preparazioneIl video di presentazione arriva presto: intanto trovi qui sotto il programma completo.
A chi serve
Studenti di informatica e ingegneria, programmatori che vogliono scrivere software più sicuro, chi lavora o vuole lavorare in avionica, ferrovie, spazio, difesa e sistemi embedded
Cosa serve per iniziare
- Un computer Windows, Mac o Linux
- Nessuna esperienza di programmazione
- Voglia di scrivere programmi precisi: in Ada il compilatore è severo, ma è dalla tua parte
Cosa installare
GNAT (compilatore Ada) con AlireGratuito. Alire (alire.ada.dev) è il gestore ufficiale della comunità: scarica il programma "alr" e con alr toolchain --select installa GNAT e gprbuild. Su Linux puoi anche usare sudo apt install gnat gprbuild
Visual Studio Code con l'estensione Ada & SPARKEditor gratuito da code.visualstudio.com; l'estensione "Ada & SPARK" di AdaCore dà colori, completamento e controllo degli errori
AdaCore Learn (editor online)Il sito learn.adacore.com contiene corsi interattivi gratuiti e un editor che compila ed esegue Ada e SPARK direttamente dal browser: ideale per provare senza installare nulla
GNATprove (per la parte SPARK)Strumento di verifica formale, gratuito, disponibile come pacchetto in Alire. Serve solo nell'ultima lezione
A cosa ti serve
- Aeronautica e avionica: software di bordo e controllo del volo
- Ferrovie e metropolitane: segnalamento e sicurezza della circolazione
- Spazio e difesa: satelliti, razzi, radar, sistemi militari
- Sistemi embedded e industria: controllo di macchine, dispositivi medici, energia
- Ruoli di analista e sviluppatore di software critico, verifica e certificazione (aziende dei settori aerospazio e trasporti)
Programma del corso
10 lezioni in 3 livelli. Ogni lezione: video, spiegazione, codice da copiare o provare, esercizio con soluzione e quiz.
1
Base
Il primo programma, i tipi forti, le decisioni, i cicli e le procedure
1Cos'è Ada e il tuo primo programmaCapire perché Ada è usato nei sistemi critici, installare GNAT e compilare il primo programma.Gratis20 min2Variabili e tipi fortiDichiarare variabili e costanti, usare i tipi base e capire perché Ada obbliga alle conversioni esplicite.Gratis25 min3Decisioni e cicliUsare if, case e i tre tipi di ciclo (for, while, loop con exit).25 min4Procedure e funzioniDividere il programma in procedure e funzioni e capire le modalità in, out e in out dei parametri.25 min
2
Intermedio
Pacchetti, dati strutturati, eccezioni e contratti
1Pacchetti: specifica e corpoOrganizzare il codice in pacchetti con specifica (.ads) e corpo (.adb) e compilare programmi su più file.30 min2Record, array, enumerazioni e contenitoriDescrivere dati complessi con record, array indicizzati, tipi enumerativi e usare i contenitori della libreria standard.35 min3Eccezioni e contrattiGestire gli errori con le eccezioni e scrivere contratti con precondizioni e postcondizioni.35 min
3
Avanzato
Tipi privati, generici, concorrenza e sistemi critici con cenni di SPARK
1Tipi privati, generici e oggettiNascondere i dettagli dei tipi, scrivere codice generico e conoscere la programmazione a oggetti di Ada.35 min2Concorrenza: task e oggetti protettiScrivere programmi con più attività in parallelo usando task e oggetti protetti, e conoscere i rendez-vous e il profilo Ravenscar.40 min3Sistemi critici e SPARKCapire come Ada entra nei sistemi certificati, conoscere i cenni di SPARK per la verifica formale e sapere come costruire un percorso di lavoro.40 min
Progetto finale: Monitor della temperatura di una cella frigorifera
Un programma che elabora una giornata di letture di temperatura di una cella frigorifera di un negozio alimentare, valuta lo stato di ogni lettura (normale, attenzione, allarme) e conta gli allarmi. È una simulazione al computer: non collegarla a impianti reali.
I passi
- Definisci un tipo enumerativo Stato (Normale, Attenzione, Allarme) e un sottotipo Temperatura con intervallo da -40.0 a 40.0 gradi.
- Scrivi una function Valuta che riceve una Temperatura e restituisce lo Stato (sopra 5 gradi attenzione, sopra 8 allarme).
- Metti la function in un pacchetto Cella, con specifica e corpo in file separati.
- Usa un array di letture e un ciclo for sul suo 'Range per valutarle tutte; conta gli allarmi.
- Aggiungi un contratto: Pre sulle letture (nell'intervallo) e Post sul risultato; compila con -gnata.
- Gestisci con un'eccezione le letture non valide e mostra un messaggio chiaro.
- Estensione: simula il sensore con un task e conserva l'ultima lettura in un oggetto protetto.
Esame e attestato
Alla fine del corso fai l'esame: 15 domande, serve il 75% di risposte giuste. Superato l'esame ottieni l'attestato stampabile con nome, ore, punteggio e un codice di controllo che chiunque può verificare.
Glossario di Ada
- Ada
- Linguaggio nato per il software affidabile e critico, con tipi forti, concorrenza e contratti.
- GNAT
- Il compilatore Ada libero, parte della collezione GCC.
- Alire
- Gestore di pacchetti e progetti Ada: crea, compila e installa strumenti e librerie.
- Tipo forte
- Tipo che il compilatore non mescola con altri senza conversioni esplicite.
- Sottotipo
- Tipo ottenuto limitando un altro tipo a un intervallo di valori, come 18 .. 30.
- Pacchetto
- Unità di codice con una specifica (.ads) visibile e un corpo (.adb) con l'implementazione.
- Eccezione
- Evento d'errore che interrompe il flusso normale e passa il controllo a un gestore.
- Contratto
- Insieme di precondizione (Pre) e postcondizione (Post) che descrivono cosa serve e cosa garantisce un sottoprogramma.
- Tipo privato
- Tipo i cui dettagli interni sono nascosti a chi usa il pacchetto.
- Generico
- Modello di sottoprogramma o pacchetto con parametri formali, riempiti quando si crea un'istanza.
- Task
- Attività che gira in parallelo con altre nello stesso programma.
- SPARK
- Sottoinsieme di Ada con strumenti di verifica formale che dimostrano matematicamente l'assenza di certi errori.
Le prime 2 lezioni sono gratis
Per il corso completo, scuole e aziende: chiedi le condizioni.