scholarly journals A Semantic Framework for Program Debugging

10.29007/q2h6 ◽  
2018 ◽  
Author(s):  
Wei Li
Keyword(s):  
Operational Semantics ◽  
Test Case ◽  
Main Task ◽  
Semantic Framework ◽  
Program Debugging ◽  
Design Error ◽  
Automated Debugging ◽  
Different Types ◽  
Structural Operational Semantics ◽  
Logical Design

This work aims to build a semantic framework for automated debugging. A debugging process consists of tracing, locating, and fixing processes consecutively. The first two processes are accomplished by a tracing procedure and a locating procedure, respectively. The tracing procedure reproduces the execution of a failed test case with well-designed data structures and saves necessary information for locating bugs. The locating procedure will use the information obtained from the tracing procedure to locate ill-designed statements and to generate a fix-equation, the solution of which is a function that will be used to fix the bugs. A structural operational semantics is given to define the functions of the tracing and locating procedure. Both procedures are proved to terminate and produces one fix-equation. The main task of fixing process is to solve the fix-equation. It turns out that for a given failed test case, there exist three different types of solutions: 1. the bug is solvable, there exists a solution of the fix-equation, and the program can be repaired. 2. There exists a non-linear error in the program, the fix-equation generated at each round of the locating procedure is solvable, but a new bug will arise when the old bug is being fixed. 3. There exists a logical design error and the fix-equation is not solvable.

scholarly journals Semantics, Modularity, and Rewriting Logic

1998 ◽  
Vol 5 (42) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Rewriting Logic ◽  
Semantic Description ◽  
Semantic Framework ◽  
Action Semantics ◽  
Strong Indicator ◽  
Hybrid Framework ◽  
Structural Operational Semantics ◽  
Modular Monadic Semantics

A complete formal semantic description of a practical programming language (such as Java) is likely to be a lengthy document, regardless of which semantic framework is being used. Good modularity of the description is important to the person(s) developing it, to facilitate reuse, change, and extension. Unfortunately, the conventional versions<br />of the major semantic frameworks have rather poor modularity.<br /> In this paper, we first recall some approaches that improve the modularity of denotational semantics, namely action semantics, modular monadic semantics, and a hybrid framework that combines these: modular monadic action semantics. We then address the issue of modularity in operational semantics, which appears to have received comparatively little attention so far, and report on some preliminary investigations of how one might achieve the same kind of modularity in structural operational semantics as the use of monad transformers<br />can provide in denotational semantics|this is the main technical contribution of the paper. Finally, we briefly consider the representation of structural operational semantics in rewriting logic, and speculate on the possibility of using it to interpret programs in the described language. Providing powerful meta-tools for such semantics-based interpretation<br />is an interesting potential application of rewriting logic;<br />good modularity of the semantic descriptions may be crucial for the practicality of using the tools.<br />Much of the paper consists of (very) simple examples of semantic descriptions in the various frameworks, illustrating the degree of reformulation needed when extending the described language|a strong indicator of modularity. Throughout, it is assumed that the reader has some familiarity with the concepts and notation of denotational and structural operational semantics. Familiarity with the basic notions of monads and monad transformers is not a prerequisite.

scholarly journals Persistent Stochastic Non-Interference

2021 ◽  
Vol 181 (1) ◽  
pp. 1-35
Author(s):  
Jane Hillston ◽  
Andrea Marin ◽  
Carla Piazza ◽  
Sabina Rossi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Evaluation Process ◽  
Decision Algorithm ◽  
Secure Systems ◽  
Information Flow Security ◽  
Structural Operational Semantics ◽  
Timing Properties ◽  
Functional Point ◽  
Security Property

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

Sign in / Sign up

Export Citation Format

Share Document