Browsing by Subject "Programming languages (Electronic computers)--Semantics"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
Item Expressiveness of answer set languages(2007) Ferraris, Paolo, 1972-; Lifschitz, VladimirAnswer set programming (ASP) is a form of declarative programming oriented towards difficult combinatorial search problems. It has been applied, for instance, to plan generation and product configuration problems in artificial intelligence and to graph-theoretic problems arising in VLSI design and in historical linguistics. Syntactically, ASP programs look like Prolog programs, but the computational mechanisms used in ASP are different: they are based on the ideas that have led to the development of fast satisfiability solvers for propositional logic. ASP is based on the answer set/stable model semantics for logic problems, originally intended as a specification for query answering in Prolog. From the original definition of 1988, the semantics was independently extended by different research groups to more expressive kinds of programs, with syntax and semantics that are incompatible with each other. In this thesis we study how the various extensions are related to each other. In order to do that, we propose another definition of an answer set. This definition has three main characteristics: (i) it is very simple, (ii) its syntax is more general than the usual concept of a logic program, and (iii) strong theoretical tools can be used to reason on it. About (ii), we show that our syntax allows constructs defined in many other extensions of the answer sets semantics. This fact, together with (iii), allows us to study the expressiveness of those constructs. We also compare the answer set semantics with another important formalism developed by Norm McCain and Hudson Turner, called logic.Item Formal specification and verification of a JVM and its bytecode verifier(2006) Liu, Hanbing; Moore, J Strother, 1947-How do we know that a bytecode-verified Java program will run safely? This dissertation addresses the question by building a precise model of the JVM and its bytecode verifier. We also built a “small” machine and its bytecode verifier to demonstrate an approach to solving this problem. We proved that for any program on the small machine that has been vetted by the small bytecode verifier, then that program will run safely on the small machine. We created substantial libraries of ACL2 definitions and lemmas towards specifying and proving that the JVM safely executes verified programs. The fundamental problem is to connect the abstract execution of the bytecode verifier with the concrete execution of the JVM. These diverge in two ways: (1) the bytecode verifier executes on more abstract states and (2) its execution of INVOKE-family and BRANCH-family instructions differs from their execution by the JVM. Our contribution was identification of a critical “on-track” property that, despite these divergences between the bytecode verifier and the JVM, enables one to use the success of bytecode verification to predict the safety of concrete execution. The second difficulty is that the official specification describes many “procedural” aspects of the bytecode verification process. These aspects obscure the checks conducted by the bytecode verifier. We introduce an alternative bytecode verifier without such “procedural” aspects. We use the new bytecode verifier as a stepping stone for proving that the official bytecode verifier is effective. Following this methodology allowed us to prove, on our ”small” machine, that executions of bytecode-verified programs never overflow the operand stack. We note that significant effort is required in order to extend this result from our “small” machine to the full JVM. We have formulated appropriate stronger notions of “safe” execution for programs on the full JVM. We introduced an alternative bytecode verifier. We proved the “reduction theorem” that relates the official bytecode verifier with the alternative bytecode veri- fier. We completed proofs of several thousand lemmas towards proving the “safe” execution of bytecode-verified programs on the full JVM. Our results are organized into supporting lemma libraries.Item Theory and applications of answer set programming(2002) Erdem, Esra; Lifschitz, Vladimir