Formalmente verificar la corrección de un algoritmo

Question

Primero de todo, es que esto sólo es posible en los algoritmos de los que no tienen efectos secundarios?

En segundo lugar, si me pueden aprender acerca de este proceso, los buenos libros, artículos, etc?

Answer 1

COQ es un asistente prueba de que produce una salida ocaml correcta. Es bastante complicado sin embargo. Nunca llegué a mirarlo, pero mi compañero de trabajo empecé y luego se dejó de usar después de dos meses. Fue sobre todo porque quería hacer las cosas más rápido, pero si usted necesita para verificar un algoritmo que esto podría ser una buena idea.

Aquí está una supuesto que utiliza COQ y habla de probar algoritmos.
Y aquí es un tutorial sobre cómo escribir trabajos académicos en COQ.

Answer 2

1. Es generalmente mucho más más fácil para verificar / comprobar la corrección cuando se trata de ningún efecto secundario, pero no es un requisito absoluto.
2. Es posible que desee ver en algunos de los documentos de un lenguaje de especificación formal como Z . Una especificación formal no es una prueba en sí, pero a menudo es la base para uno.

Answer 3

Por lo general, las pruebas de corrección son muy específicos para el algoritmo en cuestión.

Sin embargo, existen varios trucos conocidos que se utilizan y reutilizan de nuevo. Por ejemplo, con algoritmos recursivos puede utilizar invariantes de bucle .

Otro truco común es reducir el problema original a un problema para el que la prueba de su algoritmo de corrección es más fácil mostrar, a continuación, la generalización ya sea el problema más fácil o lo que demuestra que el problema más fácil puede ser traducido a una solución al problema original. Aquí es una descripción.

Si usted tiene un algoritmo particular en mente, usted puede hacerlo mejor en preguntar cómo construir una prueba de que el algoritmo en lugar de una respuesta general.

Answer 4

Comprar estos libros: http://www.amazon.com/Science-Programming -Monographs-ordenador / dp / 0387964800

Los Gries libro, Programación Científica es una gran cosa. Paciente, minuciosa y completa.

Answer 5

creo que verificar la exactitud de un algoritmo sería validar su conformidad con una especificación. Hay una rama de la informática teórica llamada Métodos formales que puede ser lo que usted está buscando, si que necesita para llegar lo más cerca a la prueba como pueda. De Wikipedia,

  

Los métodos formales son un tipo particular   de técnicas basadas matemática para el   la especificación, desarrollo y   verificación de software y hardware   sistemas

será capaz de encontrar muchos recursos de aprendizaje y herramientas de la multitud de enlaces en la página vinculada Wikipedia y de la Métodos formales wiki .

Answer 6

Lógica en Informática, por Huth y Ryan, da una visión razonablemente legible de los modernos sistemas de verificación de sistemas. Érase una vez que la gente hablado de probar los programas correcta - con los lenguajes de programación que puede o no tener efectos secundarios. La impresión que tengo de este libro y en otros lugares es que las aplicaciones reales son diferentes - por ejemplo, lo que demuestra que un protocolo es correcta, o que la unidad de coma flotante de un chip puede dividir correctamente, o que una rutina libre de bloqueo para manipular las listas enlazadas es correcta.

ACM Computing Surveys Vol 41 Número 4 (octubre de 2009) es un número especial sobre la verificación del software. Parece que se puede llegar a al menos uno de los papeles sin una cuenta ACM mediante la búsqueda de "Métodos formales: Práctica y experiencia".

Answer 7

La herramienta Frama-C , para lo cual sugiere Elazar un vídeo de demostración en los comentarios, da que un lenguaje de especificación, ACSL , para la redacción de contratos de función y varios analizadores para la verificación de que una función C satisface sus propiedades de contrato y de seguridad tales como la ausencia de errores de tiempo de ejecución.

Un tutorial extendida, ACSL por ejemplo , se muestran ejemplos de algoritmos reales C se especifican y verificados, y separa las funciones de lado libre del efecto de los effectful (los del lado-libre de efectos se consideran más fácil y vienen primero en el tutorial). Este documento también es interesante ya que no fue escrito por los diseñadores de las herramientas se describen, por lo que da un aspecto más fresco y más didáctico en estas técnicas.

Answer 8

Si está familiarizado con LISP, entonces debería salir ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html

Answer 9

Dijkstra La disciplina de la programación y sus EWDs sentar las bases para la verificación formal como una ciencia en la programación. Un trabajo más sencillo es Wirth Programación sistemática , que comienza con el enfoque simple de utilizar la verificación. Wirth usos pre-ISO Pascal para el idioma; Dijkstra utiliza un Algol-68-como el formalismo llamado vigilado (GCL). La verificación formal ha madurado desde Dijkstra y Hoare, pero estos textos antiguos todavía puede ser un buen punto de partida.

Answer 10

herramienta PVS desarrollado por los chicos de Stanford es un sistema de especificación y verificación. Trabajé en él y me pareció muy útil para Theoram de pruebas.

Answer 11

WRT (1), probablemente tendrá que crear un modelo de algoritmo de una manera que "captura" de los efectos secundarios del algoritmo en un programa de la variable de la intención de modelo de estado basado en efectos secundarios.