La familia Larch de lenguajes de especificación formal está destinada a la especificación precisa de sistemas informáticos. Permiten la especificación limpia de programas de computadora y la formulación de pruebas sobre el comportamiento del programa. [1]
La familia Larch se desarrolló principalmente en los Estados Unidos en las décadas de 1980 y 1990, con la participación de investigadores de Xerox PARC , DEC Systems Research Center (DEC / SRC), Massachusetts Institute of Technology (MIT) y otros lugares. A diferencia de la notación Z , la familia Larch tiene un lenguaje para la especificación algebraica de tipos de datos abstractos (el lenguaje compartido Larch (LSL)) y un lenguaje de interfaz separado adaptado a cada idioma en el que se escribirán los programas, como C , Modula -3 , Smalltalk, etc. El proyecto Alerce también desarrolló herramientas para respaldar el uso de especificaciones formales, incluido el Probador de Alerce (LP).