È prassi comune trasformare le specifiche dei requisiti in logica di predicato per la programmazione funzionale?

8

Recentemente sono stato assegnato a lavorare su un piccolo progetto che viene implementato in Haskell. Provenendo da uno sfondo OO / imperativo, sono abituato a convertire requisiti / storie utente in casi d'uso e diagrammi di sequenza prima della codifica.

Tuttavia, il progetto Haskell a cui sono stato assegnato, il team preferisce trasformare i requisiti degli utenti in proposizioni / dichiarazioni di logica predicata. Sapevo che la logica veniva utilizzata nei sistemi critici per la sicurezza e nei metodi formali per l'ingegneria del software, ma non tanto nella programmazione quotidiana. È questa pratica comune nel regno FP? Dove posso saperne di più su questo?

Sembra un modo naturale di "modellare" i requisiti e derivare le "funzioni" dai predicati insieme a scrivere le specifiche del tipo necessarie per le funzioni su cui operare. Ma è così che viene fatto / consigliato nella pratica o è qualcosa di peculiare alla mia squadra?

(Ho provato a effettuare ricerche approfondite prima di porre questa domanda qui. Cercare "specifiche dei requisiti nella programmazione funzionale" (e sinonimi e combinazioni di parole chiave diverse) non porta a nulla di significativo.)

    
posta PhD 17.03.2015 - 09:28
fonte

2 risposte

1

Dirò che non è limitato alla programmazione funzionale, è più legato all'obiettivo del progetto. Utilizzando la logica del predicato (logica di ordine superiore) è possibile creare prove per la logica utilizzata nel requisito. La traduzione della logica in linguaggi funzionali è probabilmente più facile. È inoltre possibile tradurre l'implementazione del linguaggio funzionale comprovata in linguaggi procedurali per ottenere un modo comprovato di implementarlo.

Se possiamo provare il programma, non è necessario testarlo. Anche se un programma ha superato 1000 test, non è ancora dimostrato. Ovviamente, non è facile creare le dimostrazioni, quindi dobbiamo semplicemente creare test.

Potresti anche voler cercare un dimostratore di teoremi, isabelle / hol.

    
risposta data 10.06.2015 - 01:34
fonte
-1

Questo è un modo per gestire la programmazione funzionale. Tende a cadere fuori dai diagrammi di flusso e dai diagrammi del flusso di dati dei "vecchi tempi". Invece di pensare in termini di oggetti, la programmazione funzionale tende a concentrarsi su quali azioni devono essere eseguite. I dati diventano casuali, pezzetti di peluria da portare avanti per aggrapparsi a ciò che stai cercando di fare.

    
risposta data 09.06.2015 - 22:36
fonte