Symbolic analysis
Symbolic analysis is a method for making interpretations based on symbols.
.
In figure there is an object to be monitored using a traffic light. That symbol is a signal to our eyes to activate an interpretation: to wait (red light), to be alert(yellow), or to go (green) ahead. In our brains there is a formal logic to handle interpretations from traffic lights. We suggest that our brains work like an automaton in traffic lights. Sometimes, when we are in a hurry, we are questiong from ourselves: can we now go, can we now go... A detection from a traffic light causes a condition to be checked in the logic. It gives us the answer: You should wait, you should wait... Now you can go. That kind of symbol (traffic light) gives us pragmatic value, because it makes our travel safe, but still we can flexibly go further to home, work, trip etc - even when the traffic is very heavy.
That was the main principle of symbolic analysis in a nutshell.
Possible Uses for Symbolic Analysis
Symbolic Analysis written in Visual Prolog can be used in modeling typical formal systems, which meet requirements for atomisticity: formal languages, theorem provers, many mathematical packages, as well as simulation and optimization packages, where the type system has been written using Vip domains.
Obs. In PDC Prolog there are numerous examples of Prolog domains written for
Implementing a Symbol and Interpretation
Symbol is a reserved word in Visual Prolog, therefore we use the object SymbolicElement to model any Symbol.
interface symbolicElement supports symbolic, drawableElement, etc. predicates '''run: () -> clause*''' end interface symbolicElement class symbolicElement : symbolicElement constructors newModel: (string ModelName). new: (string ClassName). new: (string Name, symbolicElement ParentElement). end class symbolicElement implement symbolicElement supports symbolic inherits drawableElement, etc. facts - semantics command: clause. facts - links '''link: (linkType, SymbolicElement*)'''. end implement symbolicElement
The Symbolic Language
Clause is the base for the Symbolic Language.
interface symbolic open core domains program = clause*. clause = def(defClause); %1 definitions for classes, methods, variables... creator(createClause); %2 new class or new array ref(refClause); %3 reference to variables get(getClause); %4 method invocations set(setClause); %5 assignmenets, incr/decr path(pathClause); %6 branches val(core::value); % constants etc. domains symbolicType = basicType(..) ; _class(..). domains symbolicName = className(string); methodName(string) ... end interface symbolic
The architecture
There is a PCMEF-implementation for the symbolic analysis architecture:
- F means Foundation: The clause definition (C) is the carrier for all information in symbolic analysis.
- E means Entity: SymbolicElement (S) is the base class for all specific entities in the model.
- M means Mediator: The mediator for the model to traverse SymbolicElement's activated by user actions (A).
- C means Controller: Controller provides a set of actions (A) for some utilities to change a presentation (P) or status of elements.
- P means Presentation: Presentation (P) is a graph (G) created from model elements (S).
Summary for the Symbolic Analysis Framework for Visual Prolog
The SAM Framework creates a formal model for executing source code or any specific semantics expressed in Symbolic language as clauses. For each type of the element the domain symbolicType is defined. For each name type the domain is specified. These three definitions create a small mini computer to simulate any other computer as high abstraction.
The symbolic atomistic model is a conversion from a standard Prolog parse tree, where Prolog nodes in the tree have been replaced by links to the corresponding atoms, e.g. SymbolicElements.
Applications for the Framework
The framework can be used for simulating source code, for implementing a pie, theorem provers, troubleshooting tools, simulators, as well as many other typical Prolog implementions, where there is one holistic domain to cover the whole semantics of the system.
Related work or research
The first theories for symbolic execution has been developed for decades ago, and symbolic analysis has been used for various purposes like optimizing compilers or analyzing hardware or some specific software properties, but there have not been any solid theory to suggest, what symbolic analysis really could be. The work of this page comes from the dissertation of me (Laitila 2008): Symbolic Analysis and Atomistic Model as a Basis for a Program Comprehension Methodology.
Why to use Visual Prolog
Visual Prolog's hybrid architecture is ideal for modeling source code or any formal information, like semantic web.
- In our model we use Vip's object to encapsulate each symbol and inside it there is a command to define its semantics, which in turn calls it child symbols.
- Therefore, it creates a seamless graph, which is actually a parse tree, too.
- Simulating an atomistic symbolic model is done by activating Symbol:run(), which calls it child members according to the logic of the corresponding automaton.
- Each clause type has an automaton implemented in the run-method.
A very effective property of Visual Prolog is its inference engine when used in evaluating branches of symbols, such as BDDs or any program paths. There is no need for the programmer to keep track on backtracking logic, or any fail-logic in cases when some symbol fails in simulation or traversing (a logic primitive of the corresponding symbol can cause either false or true depending on the logic: like a traffic light).
More information
- Binary Decision Diagram, BDD
- Symbolic Analysis-Blog:[1]
- Blog about Science and IT (only in Finnish): [2]
- A book about Symbolic Analysis: [3]
written by Erkki Laitila, erkki.laitila at swmaster.fi --Eki 22:06, 15 December 2009 (CET)