Symbolic analysis - Revision history

Elizabeth Safro: /* More information */

2009-12-23T18:19:21Z

More information

← Older revision		Revision as of 20:19, 23 December 2009
Line 121:		Line 121:
	'''written by Erkki Laitila''', erkki.laitila at swmaster.fi		'''written by Erkki Laitila''', erkki.laitila at swmaster.fi
	--[[User:Erkki Laitila\|Eki]] 22:06, 15 December 2009 (CET)		--[[User:Erkki Laitila\|Eki]] 22:06, 15 December 2009 (CET)

			[[Category:Visual Prolog User Projects]]

Erkki Laitila at 18:42, 20 December 2009

2009-12-20T18:42:34Z

← Older revision		Revision as of 20:42, 20 December 2009
Line 38:		Line 38:
	inherits drawableElement, etc.		inherits drawableElement, etc.

	~~'''~~facts - semantics		facts - semantics
	command: clause~~'''~~		command: clause.

	~~'''~~facts - links		facts - links
	link: (linkType, SymbolicElement*).'''		'''link: (linkType, SymbolicElement*)'''.

	end implement symbolicElement		end implement symbolicElement
Line 79:		Line 79:
	== The architecture ==		== The architecture ==
	There is a PCMEF-implementation for the symbolic analysis architecture:		There is a PCMEF-implementation for the symbolic analysis architecture:
	# P means ~~Presentation~~: ~~Presentation~~ is ~~a graph created from model elements~~.		# F means Foundation: The clause definition (C) is the carrier for all information in symbolic analysis.
	# C means ~~Controller~~: ~~Controller provides a set of actions~~ for ~~some utilities to change status of~~ the ~~elements~~.		# E means Entity: SymbolicElement (S) is the base class for all specific entities in the model.
	# M means Mediator: The ~~static part of SymbolicElement traverses specific actions e.g. transformations~~ for the model.		# M means Mediator: The mediator for the model to traverse SymbolicElement's activated by user actions (A).
	# E means ~~Entity~~: ~~SymbolicElement is the base class~~ for ~~all specific entities in the model~~.		# C means Controller: Controller provides a set of actions (A) for some utilities to change a presentation (P) or status of elements.
	# F means ~~Foundation~~: ~~The clause defintion~~ is ~~the carrier for all information in symbolic analysis~~.		# P means Presentation: Presentation (P) is a graph (G) created from model elements (S).

	[[Image:PCMEF_Architecture.jpg]]		[[Image:PCMEF_Architecture.jpg]]
Line 115:		Line 115:
	== More information ==		== More information ==
	* Binary Decision Diagram, [http://en.wikipedia.org/wiki/Binary_decision_diagram BDD]		* Binary Decision Diagram, [http://en.wikipedia.org/wiki/Binary_decision_diagram BDD]
	* Symbolic Analysis-Blog:[http://symbolicanalysis.wordpress.com~~/2009/12/14/binary-decision-diagram-vs-symbolic-analysis~~/]		* Symbolic Analysis-Blog:[http://symbolicanalysis.wordpress.com/]
	* Blog about Science and IT (only in Finnish): [http://puhtaantieteenpuolesta.blogspot.com/]		* Blog about Science and IT (only in Finnish): [http://puhtaantieteenpuolesta.blogspot.com/]
	* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]		* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]

Erkki Laitila at 18:36, 20 December 2009

2009-12-20T18:36:43Z

← Older revision		Revision as of 20:36, 20 December 2009
Line 3:		Line 3:
	[[Image:Traffic as symbolic Processing.jpg]].		[[Image:Traffic as symbolic Processing.jpg]].

	In figure there is an [http://en.wikipedia.org/wiki/Object_%28philosophy%29 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 ~~ask~~ 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.		In figure there is an [http://en.wikipedia.org/wiki/Object_%28philosophy%29 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.		That was the main principle of symbolic analysis in a nutshell.
Line 38:		Line 38:
	inherits drawableElement, etc.		inherits drawableElement, etc.

	'''~~fact~~ - semantics		'''facts - semantics
	command: clause'''		command: clause'''

			'''facts - links
			link: (linkType, SymbolicElement*).'''

	end implement symbolicElement		end implement symbolicElement
Line 76:		Line 79:
	== The architecture ==		== The architecture ==
	There is a PCMEF-implementation for the symbolic analysis architecture:		There is a PCMEF-implementation for the symbolic analysis architecture:
			# P means Presentation: Presentation is a graph created from model elements.
			# C means Controller: Controller provides a set of actions for some utilities to change status of the elements.
			# M means Mediator: The static part of SymbolicElement traverses specific actions e.g. transformations for the model.
			# E means Entity: SymbolicElement is the base class for all specific entities in the model.
	# F means Foundation: The clause defintion is the carrier for all information in symbolic analysis.		# F means Foundation: The clause defintion is the carrier for all information in symbolic analysis.
	~~# E means Entity: SymbolicElement is the base class for all specific entities in the model.~~
	~~# M means Mediator: The static part of SymbolicElement contains the transformations and handles for Mediator.~~
	~~# C means Controller: Controller is a set of utilities to change status of the elements.~~
	~~# P means Presentation: Presentation is a graph created from model elements.~~

	[[Image:PCMEF_Architecture.jpg]]		[[Image:PCMEF_Architecture.jpg]]

Erkki Laitila at 06:58, 16 December 2009

2009-12-16T06:58:43Z

← Older revision		Revision as of 08:58, 16 December 2009
Line 1:		Line 1:
	Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [http://en.wikipedia.org/wiki/symbol symbols].		Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [http://en.wikipedia.org/wiki/symbol symbols].

	[[Image:Traffic as symbolic Processing.jpg]].		[[Image:Traffic as symbolic Processing.jpg]].
Line 95:		Line 95:
	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.		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 ==		== Why to use Visual Prolog ==

Erkki Laitila at 21:07, 15 December 2009

2009-12-15T21:07:47Z

← Older revision		Revision as of 23:07, 15 December 2009
Line 111:		Line 111:
	* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]		* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]

	written by Erkki Laitila, erkki.laitila@swmaster.fi		'''written by Erkki Laitila''', erkki.laitila at swmaster.fi
	--[[User:Erkki Laitila\|Eki]] 22:06, 15 December 2009 (CET)		--[[User:Erkki Laitila\|Eki]] 22:06, 15 December 2009 (CET)

Erkki Laitila at 21:06, 15 December 2009

2009-12-15T21:06:04Z

← Older revision		Revision as of 23:06, 15 December 2009
Line 110:		Line 110:
	* Blog about Science and IT (only in Finnish): [http://puhtaantieteenpuolesta.blogspot.com/]		* Blog about Science and IT (only in Finnish): [http://puhtaantieteenpuolesta.blogspot.com/]
	* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]		* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]

			written by Erkki Laitila, erkki.laitila@swmaster.fi
			--[[User:Erkki Laitila\|Eki]] 22:06, 15 December 2009 (CET)

Thomas Linder Puls: Image on own line

2009-12-15T06:24:57Z

Image on own line

← Older revision		Revision as of 08:24, 15 December 2009
Line 1:		Line 1:
	Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [http://en.wikipedia.org/wiki/symbol symbols]. [[Image:Traffic as symbolic Processing.jpg]].		Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [http://en.wikipedia.org/wiki/symbol symbols].

			[[Image:Traffic as symbolic Processing.jpg]].

	In figure there is an [http://en.wikipedia.org/wiki/Object_%28philosophy%29 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 ask 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.		In figure there is an [http://en.wikipedia.org/wiki/Object_%28philosophy%29 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 ask 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.

Erkki Laitila at 20:53, 14 December 2009

2009-12-14T20:53:25Z

← Older revision		Revision as of 22:53, 14 December 2009
Line 101:		Line 101:
	* Each clause type has an automaton implemented in the run-method.		* Each clause type has an automaton implemented in the run-method.

	A ~~rather~~ effective property of Visual Prolog is its inference engine when used in evaluating branches of symbols, such as BDDs. There is no need for the programmer to ~~program~~ backtracking logic, or any fail-logic in cases when some symbol fails (~~it didn't succeed because~~ of ~~a false, in~~ the corresponding symbol).		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 ==		== More information ==
	* Binary Decision Diagram, [http://en.wikipedia.org/wiki/Binary_decision_diagram BDD]		* Binary Decision Diagram, [http://en.wikipedia.org/wiki/Binary_decision_diagram BDD]
	* Symbolic Analysis-Blog:		* Symbolic Analysis-Blog:[http://symbolicanalysis.wordpress.com/2009/12/14/binary-decision-diagram-vs-symbolic-analysis/]
	[http://symbolicanalysis.wordpress.com/2009/12/14/binary-decision-diagram-vs-symbolic-analysis/]		* Blog about Science and IT (only in Finnish): [http://puhtaantieteenpuolesta.blogspot.com/]
			* A book about Symbolic Analysis: [http://www.amazon.com/Symbolic-Analysis-Basis-Program-Comprehension/dp/363916833X]

Erkki Laitila at 20:46, 14 December 2009

2009-12-14T20:46:51Z

@@ Line 1: / Line 1: @@
-Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [[symbol]]s. [[Image:Traffic as symbolic Processing.jpg]].
+Symbolic analysis is a method for making [http://en.wikipedia.org/wiki/interpretation interpretations] based on [http://en.wikipedia.org/wiki/symbol symbols]. [[Image:Traffic as symbolic Processing.jpg]].
 In figure there is an [http://en.wikipedia.org/wiki/Object_%28philosophy%29 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 ask 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.
@@ Line 19: / Line 19: @@
      predicates
-        run: () -> clause*
+        '''run: () -> clause*'''
 end interface symbolicElement
@@ Line 35: / Line 35: @@
        supports symbolic
        inherits drawableElement, etc.
 end implement symbolicElement
@@ Line 89: / Line 92: @@
 == 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.

Erkki Laitila: This page describes symbolic analysis for Visual Prolog rather shortly illustrating the philosophy, architecture and a sample of code.

2009-12-14T20:32:24Z

This page describes symbolic analysis for Visual Prolog rather shortly illustrating the philosophy, architecture and a sample of code.

← Older revision		Revision as of 22:32, 14 December 2009
Line 15:		Line 15:


	<vip>~~clauses~~		<vip>
	interface symbolicElement supports symbolic, drawableElement, etc.		interface symbolicElement supports symbolic, drawableElement, etc.

Line 43:		Line 43:


	<vip>~~clauses~~		<vip>
	interface symbolic		interface symbolic
	open core		open core
Line 51:		Line 51:

	clause =		clause =
	def(defClause); %1		def(defClause); %1 definitions for classes, methods, variables...
	creator(createClause); %2		creator(createClause); %2 new class or new array
	ref(refClause); %3		ref(refClause); %3 reference to variables
	get(getClause); %4		get(getClause); %4 method invocations
			set(setClause); %5 assignmenets, incr/decr
			path(pathClause); %6 branches
			val(core::value); % constants
	etc.		etc.

	domains		domains
	symbolicType = ...		symbolicType = basicType(..) ; _class(..).

	domains		domains
	symbolicName = ...		symbolicName = className(string); methodName(string) ...

	end interface symbolic		end interface symbolic
Line 85:		Line 88:

	== Applications for the Framework ==		== Applications for the Framework ==
	The framework can be used for simulating source code, for implementing pie's, 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.		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.