Notazione matematica dei concetti di programmazione
https://stackoverflow.com/questions/1632786
-
06-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianDomanda
Esistono molti metodi per rappresentare la struttura di un programma (come i diagrammi di classe UML ecc.). Sono interessato se esiste una convenzione che descrive i programmi in modo rigoroso e matematico. Sono particolarmente interessato all'uso della notazione matematica a questo scopo.
Un esempio : le classi sono rappresentate come insiemi (campi, proprietà) e funzioni (operando sugli elementi degli insiemi). Una classe padre "i campi sono un sottoinsieme della classe figlio". Le funzioni sono descritte in pseudocodice che deve assomigliare a questo e quello ...
Soluzione
So che Z Notation è stato utilizzato in una certa misura nella verifica formale del software, come il progetto Tokeneer .
Altri suggerimenti
Sì, esiste Floyd -Hoare Logic .
Ci sono molti modi, ma penso che la maggior parte di essi siano scomodi per esprimere la struttura poiché la struttura spesso non è esprimibile in concetti matematici predefiniti. La principale eccezione sono ovviamente i linguaggi di programmazione funzionali. Pensa a pieghe (catamorfismo), gruppi, algebra ecc.
Per la programmazione imperativa conosco l'esistenza di Z, che usa la teoria del calcolo del calcolo lambda (puro ed esteso) e la logica predicata (del primo ordine). Tuttavia, non credo sia molto conveniente. L'unico lato positivo dell'uso della matematica per esprimere la struttura è il fatto che puoi provare cose al riguardo. Ma se vuoi farlo, dai un'occhiata a JML, Spec # o Eiffel.
Dipende da ciò che stai cercando di realizzare, ma andare su questa strada con lingue specifiche può metterti nei guai.
Ad esempio, vedi la discussione-ellisse su C ++ FAQ Lite.
Questo libro applica il metodo deduttivo alla programmazione tramite programmi di affiliazione con il matematico astratto teorie che consentono loro di funzionare. [...]
Credo che Elements of Programming di Alexander Stepanov e Paul McJones, è abbastanza vicino a quello che sei cercando.
Un concetto è una descrizione di requisiti per uno o più tipi dichiarato in termini di esistenza e proprietà delle procedure, tipo attributi e funzioni di tipo definite sui tipi.
Z, che è già stato menzionato, è praticamente quello che descrivi. Ci sono alcune varianti per la modellazione orientata agli oggetti, ma penso che tu possa andare abbastanza lontano con & Quot; Z standard & Quot; schemi se si desidera modellare le classi.
C'è anche Alloy , che è più recente e ispirato a Z. La sua notazione è forse un po 'più vicina all'oggetto -orientamento. È anche analizzabile, ovvero è possibile verificare se i modelli creati soddisfano determinate condizioni, ma non può dimostrare che le proprietà siano valide, tentare di confutare in un ambito finito.
L'articolo Software affidabile in base alla progettazione è una bella introduzione alla lega e il suo simile, insieme a una tabella di strumenti simili disponibili.
Stai cercando programmazione funzionale. Esistono diversi linguaggi di programmazione funzionale e sono tutto basato su una teoria matematica fondamentale chiamata Lambda calculus . I programmi scritti in un linguaggio di programmazione funzionale come LISP sono una rappresentazione matematica di se stessi. ; -)
Esiste un linguaggio matematico che in realtà descrive un programma o piuttosto le sue operazioni. Prendi lo stato iniziale e poi trasformalo fino a raggiungere lo stato desiderato desiderato. Le trasformazioni producono il codice del programma che deve essere eseguito.
Vedi l'articolo di Wikipedia sulla logica Hoare .
L'idea di base è che per ogni funzione (non importa se la metti in una classe o in una funzione di vecchio stile), hai una condizione pre e post. Ad esempio, il presupposto può essere che si disponga di un array con >= 0 elementi. la post-condizione è che ogni elemento [i] deve essere < = elemento [j] per ogni i < = j.
La normale descrizione sarebbe " la funzione ordina l'array " ;. Ma i termini matematici ti consentono di trasformare l'input (che deve corrispondere alla precondizione) in output (che deve corrispondere alla postcondizione).
È un po 'ingombrante da usare, specialmente per programmi più complessi, ma alcuni esempi sono piuttosto impressionanti. Spesso si ottiene un codice davvero compatto che risulta piuttosto complesso ma funziona al primo tentativo.
Vorrei suggerire Algebra of Programming . È un approccio di calcolo ai programmi, usando Algebra relazionale e Galois Connections .
Se hai ulteriore interesse su questo argomento, puoi trovare un documento straordinario, qui , di Shin-Cheng Mu e Jos & # 233; Nuno Oliveira ( slide ).
L'uso di Algebra relazionale e Logica del primo ordine ha anche una bella sinergia con Alloy , Programmazione funzionale e Design by Contract (facilmente applicabile alla programmazione orientata agli oggetti).
