Future directions

Admin — Tue, 07 Sep 2010 02:03:57 GMT

←Older revision		Revision as of 02:03, 7 September 2010
(2 intermediate revisions not shown.)
Line 16:		Line 16:

	This system can also be deployed by clients in their own environment. Currently, this requires installation of the Haskell Platform, and use of a command-line interface. Neither of these are ideal. It is preferable to make available a single package to users that contains both the system and any necessary supporting environment. This may require recoding (or compiling) the entire system in a different language or on a different platform.		This system can also be deployed by clients in their own environment. Currently, this requires installation of the Haskell Platform, and use of a command-line interface. Neither of these are ideal. It is preferable to make available a single package to users that contains both the system and any necessary supporting environment. This may require recoding (or compiling) the entire system in a different language or on a different platform.
		+
		+	== Integration with existing systems ==
		+
		+	Because the primary purpose of the system is to act as a user-friendly interface for verification capabilities, it is natural to implement translations that transform the inferences performed by the system's validation procedure into proofs that can be verified with some other existing verification system. This would require the creation of a back-end component that generates formal proofs that can be verified by Mizar, an instantiation of Isabelle, or even Coq. It would also be necessary to assemble a static context of propositions that corresponds to the target system. Such an exercise would enhance our system's usefulness by allowing users to validate their arguments with respect to a well-established system. It would also provide a way to further evaluate the usability benefits provided by our system. It would also potentially foster more interaction with the formal verification community.

	== Applications ==		== Applications ==

-	The approaches adopted in the development of this system can be applied more widely. For example, it should be possible to assemble a static context for particular programming languages. This context might include code templates corresponding to particular common practices or strategies. Such a variant of this system would overlap in motivation and approach to related work [1,2,3].	+	The approaches adopted in the development of this system can be applied more widely. The system's static context can be instantiated with concepts and propositions from a particular domain. It would then be possible evaluate whether there are any benefits within that context of the immediate feedback and lightweight validation provided by our system.
		+
		+	For example, it should be possible to assemble a static context for particular programming languages. This context might include code templates corresponding to particular common practices or strategies, and propositions that deal with high-level characteristics of user programs. These characteristics may include termination, unused variables, dead code, and others studied in the programming language design and optimization literature. This effort could be further bolstered by developing a separate parser that can accommodate the syntax of the programming language being considered. Such a variant of this system would overlap in motivation and approach to related work [1,2,3].
		+
		+	As another example, it should be possible to assemble a static context of concepts and facts about a family of constraints used within a particular discipline, such as control theory.

	== References ==		== References ==

Automated Assistance for Formal Reasoning - Recent changes [en]

Future directions