scholarly journals Symbolic execution formally explained

2021 ◽  
Author(s):  
Frank S. de Boer ◽  
Marcello Bonsangue
Keyword(s):  
Programming Language ◽  
Symbolic Execution ◽  
Operational Semantics ◽  
Object Oriented ◽  
Fixed Number ◽  
Transition System ◽  
Basic Object ◽  
Formal Framework ◽  
Recursive Procedures ◽  
Soundness And Completeness

AbstractIn this paper, we provide a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values.We first introduce a formalmodel for a basic programming languagewith a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we present a more general formal framework for proving the soundness and completeness of the symbolic execution of a basic object-oriented language which features dynamically allocated variables.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.

scholarly journals Baby Modula-3 and a theory of objects

1994 ◽  
Vol 4 (2) ◽  
pp. 249-283 ◽  
Author(s):  
Martin Abadi
Keyword(s):  
Programming Language ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
Denotational Semantics ◽  
Object Oriented Programming ◽  
The Core ◽  
Functional Object ◽  
Oriented Programming Language

AbstractBaby Modula-3 is a small, functional, object-oriented programming language. It is intended as a vehicle for explaining the core of Modula-3 from a biased perspective: Baby Modula-3 includes the main features of Modula-3 related to objects, but not much else. To the theoretician, Baby Modula-3 provides a tractable, concrete example of an object-oriented language, and we use it to study the formal semantics of objects. Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2004 ◽  
Vol 11 (5) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.

Digital Image Processing for Detecting and Classifying Plant Diseases

2017 ◽  
Vol 2 (11) ◽  
pp. 1-7
Author(s):  
Izay A. ◽  
Onyejegbu L. N.
Keyword(s):  
Image Processing ◽  
Fuzzy Logic ◽  
Programming Language ◽  
Design Methodology ◽  
Fuzzy Logic Controller ◽  
Object Oriented ◽  
Plant Diseases ◽  
Analysis And Design ◽  
Crop Diseases ◽  
Growing Population

Agriculture is the backbone of human sustenance in this world. With growing population, there is need for increased productivity in agriculture to be able to meet the demands. Diseases can occur on any part of a plant, but in this paper only the symptoms in the fruits of a plant is considered using segmentation algorithm and edge/ sizing detectors. We also looked at image processing using fuzzy logic controller. The system was designed using object oriented analysis and design methodology. It was implemented using MySQL for the database, and PHP programming language. This system will be of great benefit to farmers and will encourage them in investing their resources since crop diseases can be detected and eliminated early.

AN OPERATIONAL SEMANTICS FOR THE PARALLEL LANGUAGE EDEN

2002 ◽  
Vol 12 (02) ◽  
pp. 211-228 ◽  
Author(s):  
MERCEDES HIDALGO-HERRERO ◽  
YOLANDA ORTEGA-MALLÉN
Keyword(s):  
Operational Semantics ◽  
Transition System ◽  
Lazy Evaluation ◽  
Parallel Language ◽  
Parallel Processes ◽  
System A ◽  
Independent Evaluation ◽  
Level Transition ◽  
Concurrent Algorithms ◽  
Main Thread

The functional parallel language Eden — suitable for the description of parallel and concurrent algorithms in a distributed setting — is an extension of Haskell with a set of coordination features. In this paper we present a formal operational semantics for the kernel of Eden, or more precisely, for a λ-calculus widened with explicit parallelism and potentially infinite communication channels. Eden overrides the lazy nature of Haskell on behalf of parallelism. This interplay between laziness and eagerness is accurately described by the semantics proposed here, which is based on Launchbury's natural semantics for lazy evaluation, and is expressed through a two-level transition system: a lower level for the local and independent evaluation of each process, and an upper one for the coordination between all the parallel processes in the system. As processes are created either under demand or in a speculative way, different scheduling strategies are possible — ranging from a minimal one that only allows the main thread to evolve, to a maximal one that evolves in parallel every active binding.

Adding Prolog Rules and OOPs Inheritance to Legacy Databases

1991 ◽  
Author(s):  
Art Goldschmidt ◽  
Dipayan Gangopadhyay
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Object Oriented ◽  
Database System ◽  
Storage Management ◽  
Complex Objects ◽  
Rule Based ◽  
System Product ◽  
Viable Approach ◽  
Trigger Mechanisms

Abstract We present a viable approach to add rules capability or object orientation to legacy databases. Using a combination of language compilation, run-time trigger mechanisms and inter-language call facility, we integrate an object-oriented logic programming language, called OOLP, with an existing CIM Database System Product, IBM’s CIM CDF. The result is a system that provides storage management of complex objects, rule-based validation, object oriented knowledge modelling and declarative query capability.

Sign in / Sign up

Export Citation Format

Share Document