Automatic Construction of Java Programs from Functional Program Specifications
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2015, Vol 6, Issue 4
Abstract
This paper presents a novel approach to construct Java programs automatically from the input functional program specifications on natural numbers from the constructive proofs of the input specifications using an inductive theorem prover called Poiti'n. The construction of a Java program from the input functional program specification involves two phases. The theorem prover is used to construct a higher order functional (HOF) program from the input specification expressed as an existential theorem. A set of mapping rules for a Programming Language Translation System (PLTS) is defined for translating functional expressions to their semantic equivalent Java code. The generated functional program is translated into intermediate Java code in the form of a Java function using the PLTS module. The generated Java function requires a small refinement to obtain a syntactically correct Java function. This Java function is encapsulated within a user defined Java class as a member operation, which is invoked within a Java application class consisting of a main function by creating objects resulting in an executable Java program. The constructed functional program and the generated Java program both are correct with respect to the input specification as they produce the same output.
Authors and Affiliations
Md. Kabir
Keywords
Related Articles
- EP ID EP132443
- DOI 10.14569/IJACSA.2015.060409
- Views 83
- Downloads 0
Mobile Forensic Images and Videos Signature Pattern Matching using M-Aho-Corasick
Mobile forensics is an exciting new field of research. An increasing number of Open source and commercial digital forensics tools are focusing on less time during digital forensic examination. There is a major issue affe...
Improvement of Secret Image Invisibility in Circulation Image with Dyadic Wavelet Based Data Hiding with Run-Length Coded Secret Images of Which Location of Codes are Determined with Random Number
An attempt is made for improvement of secret image invisibility in circulation images with dyadic wavelet based data hiding with run-length coded secret images of which location of codes are determined by random number....
Performance Evaluation of Adaptive Virtual Machine Load Balancing Algorithm
The conception of Cloud computing has not only reshaped the field of distributed systems but also extend businesses potential. Load balancing is a core and challenging issue in Cloud Computing. How to use Cloud com...
Risk Diffusion Modeling and Vulnerability Quantification on Japanese Human Mobility Network from Complex Network Analysis Point of View
The human mobility networks are vital infrastructure in recent social systems. Many efforts have been made to keep the healthy human mobility flows to maintain sustainable development of recent well-connected society. Ho...
Agent based Bandwidth Reservation Routing Technique in Mobile Ad Hoc Networks
In mobile ad hoc networks (MANETs), inefficient resource allocation causes heavy losses to the service providers and results in inadequate user proficiency. For improving and automating the quality of service of MA...