Programación Correcta - Historial de revisiones

Carlos idict: Texto reemplazado: «
» por «»

2019-08-31T04:40:47Z

Texto reemplazado: «<div align="justify">» por «»

Anabel jc.hlg: /* Lógica de hoare */

2012-02-27T18:18:30Z

‎Lógica de hoare

Cardet0302 jc en 14:37 6 sep 2011

2011-09-06T14:37:58Z

Reynier idict en 16:13 23 may 2011

2011-05-23T16:13:45Z

Naty05024jc: Página creada con '
{{Definición |nombre=Programación Correcta |imagen=Programacion1.jpg |tamaño= |concepto= Forma correcta de programar en cualquier lenguaje.}} '''Progr...'

2011-04-29T18:13:24Z

Página creada con '<div align="justify"> {{Definición |nombre=Programación Correcta |imagen=Programacion1.jpg |tamaño= |concepto= Forma correcta de programar en cualquier lenguaje.}} '''Progr...'

Página nueva

<div align="justify">
{{Definición |nombre=Programación Correcta |imagen=Programacion1.jpg |tamaño= |concepto= Forma correcta de programar en cualquier lenguaje.}}

'''Programación Correcta'''. Lo correcto en programación ha ido migrando a convertirse sólo en control de calidad. Debe ser porque la programación es mucho más compleja debido al surgimiento de paradigmas que puedan lidiar con problemas más complejos. Pero también podría ser porque hemos ido siendo más diletantes cada vez descartando lo que consideramos «incómodo» en los proyectos de Ingeniería de Software.

= Los Pioneros<br> =

=== Lógica de Hoare<br> ===

<br>La lógica de Floyd-Hoare es un sistema formal publicado en [[1969|1969 por]] el científico británico Hoare en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de [[Robert Floyd|Robert Floyd]] para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo. <br><br>

= Teoría de Pruebas<br> =

<br>Estas teorías estaban basadas en la [[Teoría de Pruebas|Teoría de Pruebas]], que es una rama de la lógica matemática que establece que las pruebas son objetos matemáticos formales. William Alvin Howard estableció una correspondencia entre la lógica de la intuición y el cálculo lambda. Es decir, entre programas de computadoras y la lógica de pruebas. El cálculo lambda fue desarrollado por Haskell Curry y es un modelo análogo a la [[Máquina de Turing|Máquina de Turing]]. <br><br>

= Dijkstra<br> =

En 1968 publica un el artículo «Un caso en contra de la instrucción GOTO» que sirvió de base al paradigma de la [[Programación Estructurada|Programación Estructurada]].  Este artículo fue publicado en la revista Communications of the ACM con el título Go To Statement Considered Harmful (La instrucción GOTO considerada dañina) porque el editor Niklaus Wirth lo cambió. Wirth es el autor del lenguaje Pascal (entre algunos otros) y lo diseñó porque los que existían no le servían para cómo él quería enseñar la programación. Philippe Kahn fue su alumno. En 1975 Dijkstra extiende la lógica de Hoare con un método para definir la semántica de un lenguaje de programación imperativa asignando a cada comando en el lenguaje un transformador de predicado correspondiente. A diferencia de muchos otros formalismos semánticos, éste no fue diseñado como una investigación de los fundamentos de la computación. Más bien, tiene el propósito de proveer a los programadores de una metodología para desarrollar sus programas como correctos por construcción en un «estilo calculacional». Desde los 70s, el mayor interés de Dijkstra se centró en la Verficación Formal .La opinión en aquel momento era que primero se debía escribir un programa y entonces proveer una prueba matemática de verificación de cuan correcto era. Sus primeras teorías apuntaban a especificar matemáticamente lo que se suponía que el programa debía hacer e ir aplicando transformaciones matemáticas a esta especificación hasta que se conviertiera en un programa que pudiera ser ejecutado. El programa resultante es entonces conocido como «correcto por construcción». La mayoría de los trabajos posteriores de Dijkstra se preocupan por modernizar este argumento matemático. En una entrevista en el 2001, establece el deseo por la .elegancia., por lo cual el enfoque correcto sería procesar mentalmente ideas en vez de intentar .manufacturar. los programas hasta que estuvieran completos. Es de notar que esta evolución de Dijkstra tiende a poner por encima la Teoría del Conocimiento de las matemáticas formales. Aunque hay que aclarar que toda la lógica formal es una aplicación de las matemáticas a la primera. <br>

<br>

= Teoría del Conocimiento<br> =

Se pueden encontrar referencias de cómo la Teoría del Conocimiento se aplica a la Programación. Por ejemplo, se presenta a Concept Programming como un paradigma aparte que se basa en cómo se traducen los conceptos que que viven en la cabeza de los programadores a representaciones del espacio de código. En mi opinión, la programación correcta siempre es así. <br>

<br>

= Fuentes<br> =

*[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]
*[http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 Lógica dinámica y lógica modal]
*[http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 Verificación Formal]
*[http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 ¿El final de las Ciencias de la Computación? por Dijkstra. ]
*[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html La crueldad de realmente enseñar Ciencias de la Computación por Dijkstra.]
*[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html Historia de los Lenguajes de Programación ]<br>

<br>

<br>
</div>
[[Category:Lenguajes_de_programación]]

← Revisión anterior		Revisión del 04:40 31 ago 2019
Línea 1:		Línea 1:
−	~~<div align="justify">~~	+
	{{Definición \|nombre=Programación Correcta \|imagen=Programacion1.jpg \|tamaño= \|concepto= Forma correcta de programar en cualquier lenguaje.}}		{{Definición \|nombre=Programación Correcta \|imagen=Programacion1.jpg \|tamaño= \|concepto= Forma correcta de programar en cualquier lenguaje.}}

@@ Línea 6: / Línea 6: @@
 == Lógica de hoare ==
-La lógica de Floyd-Hoare es un sistema formal publicado en [[1969|1969 por]] el científico británico Hoare en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de [[Robert Floyd|Robert Floyd]] para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo.
+La lógica de Floyd-Hoare es un sistema formal publicado en [[1969|1969 por]] el científico británico [[Charles Antony Richard Hoare|Hoare]] en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de [[Robert Floyd|Robert Floyd]] para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo.
 == Teoría de pruebas ==

@@ Línea 1: / Línea 1: @@
 <div align="justify">
 {{Definición |nombre=Programación Correcta |imagen=Programacion1.jpg |tamaño= |concepto= Forma correcta de programar en cualquier lenguaje.}}
@@ Línea 5: / Línea 4: @@
 '''Programación Correcta'''. Lo correcto en programación ha ido migrando a convertirse sólo en control de calidad. Debe ser porque la programación es mucho más compleja debido al surgimiento de paradigmas que puedan lidiar con problemas más complejos. Pero también podría ser porque hemos ido siendo más diletantes cada vez descartando lo que consideramos «incómodo» en los proyectos de Ingeniería de Software.
-= Los Pioneros<br>  =
+== Lógica de hoare ==
-=== Lógica de Hoare<br>  ===
+La lógica de Floyd-Hoare es un sistema formal publicado en [[1969|1969 por]] el científico británico Hoare en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de [[Robert Floyd|Robert Floyd]] para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo.
-<br>La lógica de Floyd-Hoare es un sistema formal publicado en [[1969|1969 por]] el científico británico Hoare en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de [[Robert Floyd|Robert Floyd]] para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo. <br><br>
+== Teoría de pruebas ==
-= Teoría de Pruebas<br>  =
+Estas teorías estaban basadas en la [[Teoría de Pruebas|Teoría de Pruebas]], que es una rama de la lógica matemática que establece que las pruebas son objetos matemáticos formales. William Alvin Howard estableció una correspondencia entre la lógica de la intuición y el cálculo lambda. Es decir, entre programas de computadoras y la lógica de pruebas. El cálculo lambda fue desarrollado por Haskell Curry y es un modelo análogo a la [[Máquina de Turing|Máquina de Turing]].
-<br>Estas teorías estaban basadas en la [[Teoría de Pruebas|Teoría de Pruebas]], que es una rama de la lógica matemática que establece que las pruebas son objetos matemáticos formales. William Alvin Howard estableció una correspondencia entre la lógica de la intuición y el cálculo lambda. Es decir, entre programas de computadoras y la lógica de pruebas. El cálculo lambda fue desarrollado por Haskell Curry y es un modelo análogo a la [[Máquina de Turing|Máquina de Turing]]. <br><br>
+== Dijkstra ==
-= Dijkstra<br>  =
+En [[1968]] publica un el artículo «Un caso en contra de la instrucción GOTO» que sirvió de base al paradigma de la [[Programación Estructurada|Programación Estructurada]].&nbsp; Este artículo fue publicado en la revista Communications of the ACM con el título Go To Statement Considered Harmful (La instrucción GOTO considerada dañina) porque el editor Niklaus Wirth lo cambió. Wirth es el autor del lenguaje Pascal (entre algunos otros) y lo diseñó porque los que existían no le servían para cómo él quería enseñar la programación. Philippe Kahn fue su alumno. En [[1975]] [[Dijkstra]] extiende la lógica de [[Hoare]] con un método para definir la semántica de un lenguaje de programación imperativa asignando a cada comando en el lenguaje un transformador de predicado correspondiente. A diferencia de muchos otros formalismos semánticos, éste no fue diseñado como una investigación de los fundamentos de la computación. Más bien, tiene el propósito de proveer a los programadores de una metodología para desarrollar sus programas como correctos por construcción en un «estilo calculacional». Desde los 70s, el mayor interés de Dijkstra se centró en la Verficación Formal .La opinión en aquel momento era que primero se debía escribir un programa y entonces proveer una prueba matemática de verificación de cuan correcto era. Sus primeras teorías apuntaban a especificar matemáticamente lo que se suponía que el programa debía hacer e ir aplicando transformaciones matemáticas a esta especificación hasta que se conviertiera en un programa que pudiera ser ejecutado. El programa resultante es entonces conocido como «correcto por construcción». La mayoría de los trabajos posteriores de Dijkstra se preocupan por modernizar este argumento matemático. En una entrevista en el 2001, establece el deseo por la .elegancia., por lo cual el enfoque correcto sería procesar mentalmente ideas en vez de intentar .manufacturar. los programas hasta que estuvieran completos. Es de notar que esta evolución de Dijkstra tiende a poner por encima la Teoría del Conocimiento de las matemáticas formales. Aunque hay que aclarar que toda la lógica formal es una aplicación de las matemáticas a la primera.
-En 1968 publica un el artículo «Un caso en contra de la instrucción GOTO» que sirvió de base al paradigma de la [[Programación Estructurada|Programación Estructurada]].&nbsp; Este artículo fue publicado en la revista Communications of the ACM con el título Go To Statement Considered Harmful (La instrucción GOTO considerada dañina) porque el editor Niklaus Wirth lo cambió. Wirth es el autor del lenguaje Pascal (entre algunos otros) y lo diseñó porque los que existían no le servían para cómo él quería enseñar la programación. Philippe Kahn fue su alumno. En 1975 Dijkstra extiende la lógica de Hoare con un método para definir la semántica de un lenguaje de programación imperativa asignando a cada comando en el lenguaje un transformador de predicado correspondiente. A diferencia de muchos otros formalismos semánticos, éste no fue diseñado como una investigación de los fundamentos de la computación. Más bien, tiene el propósito de proveer a los programadores de una metodología para desarrollar sus programas como correctos por construcción en un «estilo calculacional». Desde los 70s, el mayor interés de Dijkstra se centró en la Verficación Formal .La opinión en aquel momento era que primero se debía escribir un programa y entonces proveer una prueba matemática de verificación de cuan correcto era. Sus primeras teorías apuntaban a especificar matemáticamente lo que se suponía que el programa debía hacer e ir aplicando transformaciones matemáticas a esta especificación hasta que se conviertiera en un programa que pudiera ser ejecutado. El programa resultante es entonces conocido como «correcto por construcción». La mayoría de los trabajos posteriores de Dijkstra se preocupan por modernizar este argumento matemático. En una entrevista en el 2001, establece el deseo por la .elegancia., por lo cual el enfoque correcto sería procesar mentalmente ideas en vez de intentar .manufacturar. los programas hasta que estuvieran completos. Es de notar que esta evolución de Dijkstra tiende a poner por encima la Teoría del Conocimiento de las matemáticas formales. Aunque hay que aclarar que toda la lógica formal es una aplicación de las matemáticas a la primera. <br>
+== Teoría del conocimiento ==
-<br>
+Se pueden encontrar referencias de cómo la Teoría del Conocimiento se aplica a la Programación. Por ejemplo, se presenta a Concept Programming como un paradigma aparte que se basa en cómo se traducen los conceptos que que viven en la cabeza de los programadores a representaciones del espacio de código. En mi opinión, la programación correcta siempre es así.
-= Teoría del Conocimiento<br>  =
+== Fuentes ==
 *[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]
@@ Línea 34: / Línea 27: @@
 *[http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 ¿El final de las Ciencias de la Computación? por Dijkstra. ]
 *[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html La crueldad de realmente enseñar Ciencias de la Computación por Dijkstra.]
-*[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html Historia de los Lenguajes de Programación ]<br>
+*[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html Historia de los Lenguajes de Programación ]
 </div>
 [[Category:Lenguajes_de_programación]]