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 116
- Downloads 0
Autonomous Control of Eye Based Electric Wheel Chair with Obstacle Avoidance and Shortest Path Findings Based on Dijkstra Algorithm
Autonomous Eye Based Electric Wheel Chair: EBEWC control system which allows handicap person (user) to control their EWC with their eyes only is proposed. Using EBEWC, user can move to anywhere they want on a same...
B2C E-Commerce Fact-Based Negotiation Using Big Data Analytics and Agent-Based Technologies
The focus of this study is application of intelligent agent in negotiation between buyer and seller in B2C Commerce using big data analytics. The developed model is used to conduct negotiations on behalf of prospective b...
Automatic Optic Disc Boundary Extraction from Color Fundus Images
Efficient optic disc segmentation is an important task in automated retinal screening. For the same reason optic disc detection is fundamental for medical references and is important for the retinal image analysis applic...
Enhancement of Passive MAC Spoofing Detection Techniques
Failure of addressing all IEEE 802.11i Robust Security Networks (RSNs) vulnerabilities enforces many researchers to revise robust and reliable Wireless Intrusion Detection Techniques (WIDTs). In this paper we propo...
Lonospheric Anomalies before the 2015 Deep Earthquake Doublet, Mw 7.5 and Mw 7.6, in Peru
Two major earthquakes separated by ∼5 minutes occurred in the same fault in Peru at depths of 606.2 and 620.6 km on November 24, 2015. By using Global Ionospheric Maps (GIMs) from the Center for Orbit Determination in Eu...