Notación matemática de conceptos de programación.
https://stackoverflow.com/questions/1632786
-
06-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianPregunta
Hay muchos métodos para representar la estructura de un programa (como diagramas de clases UML, etc.). Me interesa si hay una convención que describa los programas de manera estrictamente matemática. Estoy especialmente interesado en el uso de la notación matemática para este propósito.
Un ejemplo : las clases se representan como conjuntos (campos, propiedades) y funciones (que operan en los elementos de los conjuntos). Los campos de una clase primaria son un subconjunto de la clase secundaria '. Las funciones se describen en un pseudocódigo que tiene que verse así y aquello ...
Solución
Sé que la notación Z se ha utilizado hasta cierto punto en la verificación formal de software, como el proyecto Tokeneer .
Otros consejos
Sí, lo hay, Floyd -Hoare Logic .
Hay muchas maneras, pero creo que la mayoría de ellas son inconvenientes para expresar la estructura, ya que la estructura a menudo no se puede expresar en los conceptos matemáticos predeterminados. La principal excepción es, por supuesto, los lenguajes de programación funcionales. Piense en pliegues (catamorfismo), grupos, álgebra, etc.
Para la programación imperativa, sé de la existencia de Z, que utiliza la teoría de conjuntos de cálculo lambda (pura y extendida) y la lógica de predicados (de primer orden). Sin embargo, no creo que sea muy conveniente. La única ventaja de usar las matemáticas para expresar la estructura es el hecho de que puedes probar cosas al respecto. Pero si desea hacer eso, eche un vistazo a JML, Spec # o Eiffel.
Depende de lo que intentes lograr, pero seguir este camino con idiomas específicos puede meterte en problemas.
Por ejemplo, vea la discusión círculo-elipse en C ++ FAQ Lite.
Este libro aplica el método deductivo a la programación por programas afiliados con la matemática abstracta teorías que les permiten trabajar. [...]
Creo que Elementos de programación de Alexander Stepanov y Paul McJones, está bastante cerca de lo que eres buscando.
Un concepto es una descripción de requisitos en uno o más tipos declarado en términos de la existencia y propiedades de procedimientos, tipo atributos y funciones de tipo definidas en los tipos.
Z, que ya se ha mencionado, es más o menos lo que usted describe. Hay algunas variantes para el modelado orientado a objetos, pero creo que puedes llegar bastante lejos con & Quot; Z estándar & Quot; esquemas si desea modelar clases.
También hay Alloy , que es más nuevo e inspirado en Z. Su notación está quizás un poco más cerca del objeto -orientación. También es analizable, es decir, puede verificar los modelos que crea si cumplen ciertas condiciones, pero no puede probar que las propiedades se mantengan, solo intente refutar dentro de un alcance finito.
El artículo Software confiable por diseño es una buena introducción a Alloy y su tipo, junto con una tabla de herramientas similares disponibles.
Está buscando programación funcional. Hay varios lenguajes de programación funcionales, y son todo basado en una teoría matemática fundamental llamada cálculo Lambda . Los programas escritos en un lenguaje de programación funcional como LISP son una representación matemática de sí mismos. ;-)
Hay un lenguaje matemático que realmente describe un programa o más bien sus operaciones. Toma el estado inicial y luego transforma este estado hasta que alcances el estado deseado. Las transformaciones producen el código del programa que debe ejecutarse.
Vea el artículo de Wikipedia sobre la lógica de Hoare .
La idea básica es que para cada función (no importa si la pones en una clase o en una función de estilo antiguo), tienes una condición previa y una posterior. Por ejemplo, la condición previa puede ser que tenga una matriz que tenga >= 0 elementos. la condición posterior es que cada elemento [i] debe ser < = element [j] por cada i < = j.
La descripción habitual sería " la función ordena la matriz " ;. Pero los términos matemáticos le permiten transformar la entrada (que debe coincidir con la condición previa) en la salida (que debe coincidir con la condición posterior).
Es un poco difícil de usar, especialmente para programas más complejos, pero algunos de los ejemplos son bastante impresionantes. A menudo, obtienes un código realmente compacto como resultado, que parece bastante complejo pero funciona al primer intento.
Me gustaría sugerir Álgebra de programación . Es un enfoque de cálculo para los programas, usando Relational Algebra , y Conexiones Galois .
Si tiene más interés en este tema, puede encontrar un artículo sorprendente, aquí , por Shin-Cheng Mu y Jos & # 233; Nuno Oliveira ( diapositivas ).
El uso de álgebra relacional y lógica de primer orden, también tiene una buena sinergia con Alloy , programación funcional y Diseño por contrato (se aplica fácilmente a la programación orientada a objetos).
