¿Es una práctica común transformar las especificaciones de requisitos en lógica de predicados para la programación funcional?

8

Recientemente me asignaron a trabajar en un pequeño proyecto que se está implementando en Haskell. Viniendo de un entorno OO / imperativo, estoy acostumbrado a convertir requisitos / historias de usuario en casos de uso y diagrama de secuencia antes de la codificación.

Sin embargo, en el proyecto de Haskell al que me han asignado, el equipo prefiere transformar los requisitos del usuario en proposiciones / declaraciones de lógica de predicados. Era consciente de que la lógica se usaba en sistemas críticos de seguridad y métodos formales para la ingeniería de software, pero no tanto en la programación diaria. ¿Es esta práctica común en el ámbito de FP? ¿Dónde puedo aprender más sobre esto?

Parece una forma natural de 'modelar' los requisitos y derivar las 'funciones' de los predicados junto con escribir las especificaciones de tipo necesarias para que las funciones operen. ¿Pero es así como se hace / recomienda en la práctica o es algo peculiar de mi equipo?

(He intentado buscar extensamente antes de hacer esta pregunta aquí. Buscar "especificación de requisitos en programación funcional" (y diferentes sinónimos y combinaciones de palabras clave) no conduce a nada significativo).

functional-programming requirements haskell logic formal-methods Doctor
fuente
1
cs.toronto.edu/~hehner/lsfp.pdf
Robert Harvey

Respuestas:

1

Diré que no se limita a la programación funcional, sino que está más relacionada con el objetivo del proyecto. Mediante el uso de la lógica de predicados (lógica de orden superior) puede crear pruebas para la lógica utilizada en el requisito. Traducir la lógica a lenguajes funcionales es probablemente más fácil. También es posible traducir la implementación probada del lenguaje funcional a lenguajes de procedimiento para obtener algún tipo de forma probada de implementarlo.

Si podemos probar el programa, entonces no necesitamos probarlo. Incluso si un programa pasó 1000 pruebas, aún no está probado. Obviamente, no es fácil crear las pruebas, así que solo creamos pruebas en su lugar.

También es posible que desee buscar el teorema prover, isabelle / hol.

imel96
fuente
-1

Esa es una forma de lidiar con la programación funcional. Tiende a caerse de los diagramas de flujo y diagramas de flujo de datos de los "viejos tiempos". En lugar de pensar en términos de objetos, la programación funcional tiende a centrarse en las acciones que deben realizarse. Los datos se vuelven incidentales, pedazos de pelusa para llevar a lo que estás tratando de hacer.

Joe Sewell
fuente
esto se lee más como un comentario, vea Cómo responder
mosquito
2
Lo siento. El comentario de una persona es la respuesta de otra persona. Este no es mi primer rodeo de Stack Exchange.
Joe Sewell
No estoy seguro de estar de acuerdo. La pregunta en sí va a reunir opiniones, por lo que tal vez haya problemas con la pregunta, pero creo que la respuesta realmente aborda la pregunta formulada. Los diagramas de flujo y los flujos de datos son una parte importante de las especificaciones de requisitos comerciales.
maple_shaft