Accessible Integrated Formal Reasoning Environments - Recent changes [en]

Prototype: Component Tools: SPIN

2012-05-20T06:50:57Z

New page

== Retrieval and installation ==

The latest version of SPIN can be obtained here: [http://spinroot.com/spin/Man/README.html http://spinroot.com/spin/Man/README.html].

To install SPIN on Amazon Linux (Fedora), go to the source directory and type:

yacc -v -d spin.y

Next, you may receive one or more instances of the following error:

reprosrc.c: error: "yylval" undeclared (first use in this function)

To address this, add the line <code>YYSTYPE yylval;</code> to the beginning of <code>reprosrc.c</code>, so that it looks as follows:

#include <stdio.h>
#include "spin.h"
#include "y.tab.h"
YYSTYPE yylval;

Finally, run <code>make</code> and copy the executable to the parent directory.

make
mv spin ../spin

Prototype: Development

2012-05-20T06:31:59Z

← Older revision		Revision as of 06:31, 20 May 2012
(3 intermediate revisions not shown)
Line 1:		Line 1:
	This article contains materials related to the current effort to develop a prototype accessible integrated formal reasoning environment.		This article contains materials related to the current effort to develop a prototype accessible integrated formal reasoning environment.
		+
		+	== Integration of systems: SPIN and Alloy for protocol design ==
		+
		+	This effort involves developing an infrastructure that makes it possible to use SPIN and Alloy to analyze simple protocol examples over the web. The tasks include:
		+	* defining a format for analysis requests (ARs); each analysis request should have:
		+	** the protocol definition in the target system's syntax
		+	** the properties to be checked by the system
		+	*** for each property, the response to send to the user for each possible system output
		+	* SPIN ([[Prototype: Component Tools: SPIN]])
		+	** client-side web interface
		+	*** a simple web page allowing a user to submit a Promela protocol definition, and to select one or more properties that must be checked
		+	** server-side
		+	*** installed, working version of SPIN on a server
		+	*** script (implemented in, e.g., PHP) for:
		+	**** accepting ARs as POST requests
		+	**** running SPIN on the protocol to produce an output
		+	**** returning the appropriate response to the user based on the AR
		+
		+	== Programming meta-language for automated formal algorithms and translators ==
		+
		+	This effort involves developing the high-level multi-paradigm programming language ''informl'', which is created specifically for defining common formal algorithms so that they can be compiled to run on multiple modern web platforms, including PHP servers and browsers capable of running JavaScript. This task involves:
		+	* continuing work on the language parser
		+	* implementing a library of common functions
		+	* implementing compilers
		+	** JavaScript compiler
		+	** PHP compiler
		+	*** handling globals
		+	*** converting closures
		+
		+	== Implementation of common algorithms ==
		+
		+	This effort involves implementing the following formal algorithms using the language developed in the task above. The algorithms include, among others:
		+	* monomorphic type checking
		+	* logical resolution
		+	* unification
		+	* congruence closure

MediaWiki:Sidebar

2012-05-18T06:14:53Z

Prototype: Development

2012-05-18T05:57:00Z

Created page with "This article contains materials related to the current effort to develop a prototype accessible integrated formal reasoning environment."

New page

This article contains materials related to the current effort to develop a prototype accessible integrated formal reasoning environment.

Reports and documents

2012-05-17T06:20:05Z

← Older revision	Revision as of 06:20, 17 May 2012
(One intermediate revision not shown)

User:Saber

2012-05-17T05:53:22Z

created new account User:Saber

User:Andrei

2012-05-15T20:04:35Z

changed group membership for User:Andrei from (none) to Administrators and Bureaucrats