PSICOLOGIA Y AUTOAYUDA

LA MEJOR INFORMACION Y RECURSOS WEB GRATIS DE INTERNET EN ESPAÑOL - (CASTELLANO)

 

ENCICLOPEDIA Y DICCIONARIO ONLINE - LETRA A


Término/Expresión:
 " ACL2" 
   
 Definición: 
 " ACL2 es, a la vez, un lenguaje de programacion, una logica matematica para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un demostrador automatico de teoremas que asiste al usuario en dicha tarea. ACL2 es la version industrial del demostrador NQTHM de R. Boyer y J S. Moore. En la actualidad esta desarrollado por J S. Moore y M. Kaufmann en la Universidad de Texas en Austin. El nombre ACL2 es una abreviatura de A Computational Logic for an Applicative Common LISP." 
   
 El lenguaje de programacion ACL2 es un subconjunto aplicativa de Common LISP. ACL2 es un lenguaje sin tipos debido a que todas las funciones de ACL2 son totales –es decir, toda funcion asocia a cada valor del universo de ACL2 otro valor de ese universo. Los programas escritos en ACL2 pueden ser ejecutados en Common Lisp directamente. El propio ACL2 esta desarrollado usando su mismo lenguaje aplicativo. 
   
 Una caracteristica importante de ACL2 es que se usa el mismo lenguaje tanto para la implementacion de los programas como para la especificacion de sus propiedades. La logica de ACL2 es un subconjunto de la logica de primer orden. Sus formulas no tienen cuantificadores y las variables de una formula se consideran (implicitamente) universalmente cuantificadas. La teoria de base de ACL2 axiomatiza la semantica de su lenguaje de programacion y de sus funciones predefinidas, tal y como se describen en el estandar Common Lisp. Cuando las definiciones del usuario satisfacen un cierto principio de definicion extienden la teoria con el correspondiente axioma de definicion. Grosso modo, el principio de definicion garantiza que la funcion definida termina para todas las entradas posibles, manteniendo asi la consistencia logica de la teoria. 
  
 El demostrador de ACL2 puede considerarse como un asistente para la demostracion de teoremas en la logica de ACL2. El motor de demostracion de ACL2 esta basado principalmente en la reescritura de terminos y en la automatizacion del principio de induccion. Aunque en principio ACL2 puede ser considerado un demostrador automatico (una vez introducida una conjetura, procede de manera automatica en su intento de demostracion), el sistema es interactivo en un sentido mas profundo. El papel del usuario en una formalizacion tipica con ACL2 consiste en: a) definir las funciones que implementan el sistema que se quiere verificar, b) escribir la especificacion del mismo, expresando las propiedades formales que se desean verificar y c) guiar al demostrador hacia una demostracion automatica de dicha especificacion. La manera principal mediante la cual el usuario guia al demostrador consiste en la demostracion de lemas previos que se incluyen en el sistema como reglas de reescritura y que son usados en la demostracion de posteriores resultados. Los lemas especificos necesarios para cada demostracion pueden venir sugeridos de una demostracion (manual) preconcebida o bien, a mas bajo nivel, de la inspeccion de la salida generada por un intento de demostracion automatica fallido. 
   
 El objetivo de los creadores de ACL2 fue realizar una version del demostrador NQTHM de Boyer-Moore que pudiera ser utilizado para aplicaciones de escala industrial. Por ese objetivo, ACL2 contiene muchas caracteristicas que permiten el desarrollo limpio de teorias matematicas y computacionales. Ademas, ACL2 obtiene eficiencia gracias a que esta escrito en Common LISP. Asi, la misma especificacion que es la base para una verificacion formal puede ser compilada y ejecutada en codigo nativo. 
   
 La principal aplicacion de ACL2 se encuentra en la verificacion formal de sistemas hardware cuya seguridad es critica. Dichos sistemas son modelados en el lenguaje de programacion y las propiedades que aseguran su correccion son formalmente verificadas. El hecho de que el modelo pueda ser ejecutado de manera eficiente permite ademas que pueda ser usado como un simulador del sistema modelado. 
   
 Fuente: 
 ACL2 - Wikipedia, la enciclopedia libre 
 http://es.wikipedia.org/wiki/ACL2 
   
 Más Información: 
  

IMPORTANTE: Este sitio web no admite ninguna responsabilidad derivada del uso incorrecto, inapropiado o ilícito de la información aparecida en sus páginas de Internet. Tampoco asume ninguna responsabilidad derivada de la falta de veracidad, integridad, actualización y precisión de los datos o informaciones que se contienen en sus páginas de Internet. En ningún caso, los contenidos e información son responsabilidad de este sitio web, ni constituyen opiniones, consejo psicologico, médico o asesoramiento legal de ningún tipo pues se trata meramente de un servicio ofrecido con carácter informativo y divulgativo. Consulte SIEMPRE con un Profesional.