| 1. |
|
|
| 2. |
- Bonnier, Staffan
(författare)
-
Horn clause logic with external procedures : towards a theoretical framework
- 1989
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Horn clause logic has certain properties which limit its usefulness as a programming language. In this thesis we concentrate on three such limitations: (1) Horn clause logic is not intended for the implementation of algorithms. Thus, if a problem has an efficient algorithmic solution it may be difficult to express this within the Horn clause formalism. (2) To work with a predefined structure like integer arithmetic, one has to axiomatize it by a Horn clause program. Thus functions of the structure are to be represented as predicates of the program. (3) Instead of re-implement existing software modules, it is clearly better to re-use them. To this end, a support for combining Horn clause logic with other programming languages is needed.When extending the Horn clause formalism, there is always a trade-off between general applicability and purity of the resulting system. There have been many suggestions for solving some of problems (1) to (3). Most of them use one of the following strategies: (a) To allow new operational features, such as access to low-level constructs of other languages. (b) To introduce new language constructs, and to support them by a clean declarative semantics and a complete operational semantics.In this thesis a solution to problems (1) to (3) is suggested. It combines the strategies of (a) and (b) by limiting their generality: We allow Horn clause programs to call procedures written in arbitrary languages. It is assumed however that these procedures are either functional or relational. The functional procedures yield a ground term as output whenever given ground terms as input. Similarly, the relational procedures either succeed or fail whenever applied to ground terms. Under these assumptions the resulting language has a clean declarative semantics.For the operational semantics, an extended but incomplete unification algorithm, called S-unify is developed. By using properties of this algorithm we characterize classes of goals for which our interpreter is complete. It is also formally proved that (a slightly extended version of) S-unify is as complete as possible under the adopted assumptions.
|
|
| 3. |
- Heyer, Tim, 1967-
(författare)
-
Semantic Inspection of Software Artifacts From Theory to Practice
- 2001
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Providing means for the development of correct software still remains a central challenge of computer science. In this thesis we present a novel approach to tool-based inspection focusing on the functional correctness of software artifacts. The approach is based on conventional inspection in the style of Fagan, but extended with elements of formal verification in the style of Hoare. In Hoare’s approach a program is annotated with assertions. Assertions express conditions on program variables and are used to specify the intended behavior of the program. Hoare introduced a logic for formally proving the correctness of a program with respect to the assertions.Our main contribution concerns the predicates used to expressassertions. In contrast to Hoare, we allow an incomplete axiomatization of those predicates beyond the point where a formal proof of the correctness of the program may no longer be possible. In our approach predicates may be defined in a completely informal manner (e.g. using natural language). Our hypothesis is, that relaxing the requirements on formal rigor makes it easier for the average developer to express and reason about software artifacts while still allowing the automatic generation of relevant, focused questions that help in finding defects. The questions are addressed in the inspection, thus filling the somewhat loosely defined steps of conventional inspection with a very concrete content. As a side-effect our approach facilitates a novel systematic, asynchronous inspection process based on collecting and assessing the answers to the questions.We have adapted the method to the inspection of code as well as the inspection of early designs. More precisely, we developed prototype tools for the inspection of programs written in a subset of Java and early designs expressed in a subset of UML. We claim that the method can be adapted to other notations and (intermediate) steps of the software process. Technically, our approach is working and has successfully been applied to small but non-trivial code (up to 1000 lines) and designs (up to five objects and ten messages). An in-depth industrial evaluation requires an investment of substantial resources over many years and has not been conducted. Despite this lack of extensive assessment, our experience shows that our approach indeed makes it easier to express and reason about assertions at a high level of abstraction.
|
|
| 4. |
- Maluszynski, Jan, 1941-, et al.
(författare)
-
Logic Programs with External Procedures
- 1993
-
Ingår i: Logic programming languages. - Cambridge, MA, USA : MIT Press. - 0262011344 ; , s. 21-48
-
Bokkapitel (refereegranskat)
|
|
| 5. |
- Stylianopoulos, Charalampos, 1991, et al.
(författare)
-
Industry Paper: On the Performance of Commodity Hardware for Low Latency and Low Jitter Packet Processing
- 2020
-
Ingår i: DEBS 2020 - Proceedings of the 14th ACM International Conference on Distributed and Event-Based Systems. - New York, NY, USA : ACM. ; , s. 177-182
-
Konferensbidrag (refereegranskat)abstract
- With the introduction of Virtual Network Functions (VNF), network processing is no longer done solely on special purpose hardware. Instead, deploying network functions on commodity servers increases flexibility and has been proven effective for many network applications. However, new industrial applications and the Internet of Things (IoT) call for event-based systems and midleware that can deliver ultra-low and predictable latency, which present a challenge for the packet processing infrastructure they are deployed on. In this industry experience paper, we take a hands-on look on the performance of network functions on commodity servers to determine the feasibility of using them in existing and future latency-critical event-based applications. We identify sources of significant latency (delays in packet processing and forwarding) and jitter (variation in latency) and we propose application- and system-level improvements for removing or keeping them within required limits. Our results show that network functions that are highly optimized for throughput perform sub-optimally under the very different requirements set by latency-critical applications, compared to latency-optimized versions that have up to 9.8X lower latency. We also show that hardware-aware, system-level configurations, such as disabling frequency scaling technologies, greatly reduce jitter by up 2.4X and lead to more predictable latency.
|
|
