Programmazione didattica e metodi formali

Question

Ecco una sorta di domanda strana. Sto scrivendo un libro su come imparare a programmare usando metodi formali e lo indirizzerò verso persone con qualche esperienza di programmazione. L'idea è di insegnare loro ad essere programmatori di alta qualità.

La notazione di base verrà dalla Disciplina della programmazione di Dijkstra con alcune estensioni di comunicazione e di concorrenza.

A differenza di EWD, voglio che i miei studenti alla fine scrivano veri programmi eseguibili. Ciò significa che a un certo punto la traduzione dalla notazione EWD in un'altra lingua. Quando ho iniziato a fare la programmazione formale ho preso di mira C, ma finisci per scrivere un sacco di idraulica, inoltre ci sono tutte le complessità del trattamento dei puntatori, ecc. Ruby è un ovvio obiettivo possibile, come Scheme o Lisp. Ma ci sono anche le varie lingue delle funzioni; poiché sono particolarmente interessato alla concorrenza, Erlang sembra una possibilità.

Quindi, finalmente, ecco la mia domanda: che lingua (e) dovrei insegnare ai miei lettori a indirizzare i loro programmi sviluppati formalmente?

Answer 1

Charlie,

Ho sempre associato il capolavoro di Dijkstra a un modello di programmazione in cui il palcoscenico centrale è occupato da loop e array. Se ti stai avvicinando a Dijkstra (ad esempio, calcolando i presupposti più deboli) penso che troverai che i linguaggi funzionali non sono adatti. Dei linguaggi popolari che forniscono un buon supporto per la programmazione imperativa con loop e array, forse Python trasporta il bagaglio aggiuntivo in meno.

Questo non vuol dire che i linguaggi funzionali non sono adatti ai metodi formali --- sono molto adatti --- ma lo stile è abbastanza diverso da Dijkstra. I metodi preferiti enfatizzano le prove di calcolo; vedi l'articolo di Richard Bird sulla risoluzione di Sudoku (che è pesante) o il libro di testo di Richard Bird e Phil Wadler.

Per la concorrenza dipende molto dal modello di concorrenza (e dai metodi formali) in cui si crede. La Concurrent ML di John Reppy è un bellissimo modello di trasmissione di messaggi. Erlang ha anche un bel modello pulito e restrittivo. D'altra parte, la programmazione con blocchi e sezioni critiche è così difficile che potrebbero esserci maggiori vantaggi per i metodi formali in quella situazione.

Altre due osservazioni di passaggio che potrebbero interessare la tua ricerca di base:

• L'unico programmatore che abbia mai incontrato che applicava i metodi di Dijkstra in pratica ai sistemi reali era Greg Nelson, che lavorava in Modula-3. (Greg e Mark Manasse hanno scritto insieme il sistema di finestre Trestle.) Modula-3 era un linguaggio molto carino che il digitale ha permesso di morire a causa dell'incapacità e dell'incompetenza. Greg aveva un bel documento TOPLAS su un'estensione del calcolo di Dijkstra.

• Il linguaggio di modellazione di Gerard Holzmann SPIN si basa direttamente sul linguaggio dei comandi custoditi di Dijkstra, e supporta anche la concorrenza. Il suo scopo è il controllo del modello, non la programmazione, e ci sono alcune idiosincrasie, ma c'è una forte connessione con i metodi formali ed è davvero fantastico essere in grado di modellare il controllo delle tue affermazioni. Chiunque sia interessato ai metodi formali vorrà verificarlo.

(Modifica: ecco un link al Greg Nelson carta o uno di questi. - CRM)

Answer 2

Ignorando l'ovvio qual è il tuo favorite < a href = "https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better"> programmazione language , posso vedere due risposte utili:

Da un lato, stai cercando di dimostrare i metodi a quelli che si presume siano programmatori intermedi. Se selezioni una sola lingua e la benedici come lingua dei tuoi libri, potresti alienare potenziali lettori che non capita di preferire quella lingua per una ragione o per l'altra. Dal momento che stai dimostrando metodi, hai il lusso di usare snippet in lingue che illustrano concisamente il tuo punto. Ad esempio, l'unica lingua disponibile per dimostrare RIIA è probabilmente il C ++, ma questa stessa lingua è piuttosto scarsa per mostrare come eseguire l'analisi dei sorgenti. Lo schema è ideale per l'analisi del codice sorgente, ma non offre molte opzioni per esplorare i vantaggi (e i punti deboli) della tipizzazione forte. Usa molte lingue.

D'altra parte, dato che sei principalmente interessato ai metodi di programmazione, non sono del tutto sicuro che tu abbia bisogno di un vero linguaggio. Una notazione ben definita è altrettanto buona e costringe i tuoi lettori a concentrarsi sul punto che stai facendo piuttosto che sui dettagli superficiali di una lingua o di un'altra.

Answer 3

Sono cresciuto con Lisp e Scheme e li amo entrambi. Penso che siano grandi lingue da imparare da zero. Ma non sono sicuro che qualcuno con una certa esperienza di programmazione si occuperebbe di quei linguaggi. Non otterrai molti successi su Amazon per il tuo libro con Scheme nel titolo. :)

C # è una lingua molto semplice da imparare e ha tutte le basi di cui avresti bisogno per approfondire argomenti come la concorrenza abbastanza rapidamente. Ha più applicabilità perché puoi indirizzare anche OO e concetti web. È anche abbastanza popolare e otterresti aziende che pagano per i libri dei loro dipendenti, che è sempre un bene per le vendite ("Be a Kick Ass C # Programmer") va molto più avanti in un foglio di rimborso spese rispetto a "Concurrency in Modern Lisp").

F # è un linguaggio interessante. Ha la bellezza funzionale di un Lisp o di uno Schema (beh, non del tutto, ma quasi) e ti dà la possibilità di immergerti negli argomenti OOP e di collegarti a .NET Framework per l'interfaccia utente se vuoi rendere le cose più interessanti. Ma, in questo momento, è oscuro.

Non posso parlare con Ruby, quindi personalmente morderei il proiettile e andrei con C #.

Answer 4

Onestamente, non posso raccomandare Ruby per questo. Quando programmo giorno per giorno nel mio mondo commerciale, mi piace parecchio, sicuramente molto più di C o Java. Ma la sua semantica è così mal definita che non mi fido della metà di C dove, anche se potrei passare diverse ore a discutere su una dichiarazione e a consultare quel libro bianco molto più spesso che ha sostituito K & amp; esco alla fine abbastanza convinto che se avessi un compilatore conforme (sì, lo so, sono un sognatore, ma lavoro qui con me) so cosa verrà fuori dall'altra parte.

Il rubino è meraviglioso sotto molti aspetti, ma per quanto riguarda qualsiasi cosa formale, i due non si incontreranno mai.

Tendo a votare per Haskell personalmente, perché ogni volta che mi giro mi stupisco di quanto tutto abbia senso in quella definizione linguistica. (Anche se devo ammetterlo dopo solo un anno o giù di lì, sono sicuro di non aver esplorato la metà degli angoli di Haskell 98.)

E capisco anche la Dikjstra contro la cosa funzionale; tornare indietro e leggendo i suoi articoli è molto in un mondo imperativo; Non sono qualificato per dire se è andato davvero nel modo sbagliato lì. Forse sono solo sopraffatto da quanto è buona la sua scrittura, tanto quanto il suo pensiero. Ma sembra che gli piaccia, quindi che dire dell'uso di Algol 60 ?

Answer 5

Questa è una bella idea. Penso che Scheme sia una buona opzione in quanto consente di mettere in pratica (sotto forma di librerie) diverse astrazioni con un minimo indispensabile. È anche facile tradurre dallo schema in un sistema di verifica come PVS ( http: //pvs.csl.sri. com / )

applausi

Answer 6

Penso che dovresti avere un po 'di esperienza nella lingua che usi per il tuo libro o qualcuno che sia capace di rivedere il tuo codice.

Personalmente, userei Common Lisp, dato che ne ho familiarità, ed è un ottimo linguaggio per implementare qualsiasi concetto. Altre opzioni potrebbero essere Erlang, Haskell, Ruby o Python, forse anche un dialetto ML. Sono di parte contro la famiglia C (compresi C # e Java), sembrano bloccati a un livello inferiore di pensiero sui concetti.

Answer 7

Ci sono alcune università che usano Perfect Developer per insegnare metodi formali (dichiarazione di non responsabilità: sono collegato a questo prodotto). È costruito attorno a un linguaggio per esprimere specifiche, perfezionamento dei dati e algoritmi. Ha un teorema automatico per la verifica e un generatore di codice in grado di produrre C ++, C # e Java. Il design del PD è stato molto ispirato da "Una disciplina di programmazione", tuttavia abbiamo trovato la notazione piuttosto impraticabile per i sistemi di grandi dimensioni, quindi la notazione si è leggermente discostata da quella di Dijktra.