Existing approaches to assigning semantics to procedural programming languages do not easily allow automatic reasoning over programs. We assign a model theoretic semantics to programs of a simple procedural language, by encoding them into description logics with concrete domains. This allows us to flexibly express several reasoning problems over procedural programs, and to solve them efficiently using existing reasoning algorithms, for certain fragments of the programming language. Furthermore, it allows us to explore for what further fragments of the programming language reasoning problems are decidable.
Ronald de Haan representative procedural programming language While. Then, we show how programs of this programming language can be encoded into the description logic ALC(D) in a semantically faithful way. Also, we illustrate how this allows us to encode reasoning problems over While programs into ALC(D) reasoning problems. Finally, we will discuss the benefit of this method, in combination with suggestions for further research. 2
A concrete domain D is a pair (∆ D, ΦD), where ∆ D is a set and ΦD a set of predicate names. Each predicate name P ∈ ΦD is associated with an arity n and an n-ary predicate P D ⊆ ∆ nD. A predicate conjunction of the form c = ^ (x(0i), . . . , x(nii)) : Pi,
i≤k where Pi is an ni-ary predicate, for all i ≤ k, and the x(i) are variables, is satisfiable j iff there exists a function δ mapping the variables in c to elements of ∆ D such that (δ(x(0i)), . . . , δ(x(nii))) ∈ PiD, for all i ≤ k. A concrete domain is called admissible iff its set of predicate names is closed under negation and contains a name ⊤D for ∆ D, and the satisfiability problem for finite conjunctions of predicates is decidable.
An example of an admissible concrete domain is N = (N, ΦN ), where ΦN contains unary predicates ⊤N and ρn, and binary predicates ρ, for ρ ∈ {=, 6=, <, ≤, >, ≥}, and ternary predicates +, −, ⋆, \, and the required negations of predicates. All predicates are given the usual interpretation (here ρn holds for a value x iff x ρ n holds).
We will use the description logic ALC(D) [2], which is the extension of the prototypical description logic ALC [7] with concrete domains. For an overview of description logics with concrete domains, see [3].
We get the logic ALC(D), for a given concrete domain, by augmenting ALC with abstract features (roles interpreted as functional relations), concrete features (interpreted as a partial function from the logical domain into the concrete domain), and a new concept constructor that allows to describe constraints on concrete values using predicates from the concrete domain. More concretely, we can construct concepts ∃u1, . . . , uk.P and u↑, for u, u1, . . . , uk paths and P ∈ Ψ D a k-ary predicate. A path is a sequence f1 . . . fng, where f1, . . . , fn (for n ≥ 0) are abstract features and g is a concrete feature.
Paths are interpreted as (partial) functions from the logical domain into the concrete domain, by taking the composition of the interpretation of their components. Concepts ∃u1, . . . , uk.P are interpreted as the set of objects that are in the domain of the interpretation of all ui, such that the resulting concrete objects satisfy the predicate P . Concepts u↑ are interpreted as those objects that are not in the domain of the interpretation of u. For a complete, formal definition of the syntax and semantics of ALC(D), see [2, 3], for instance. 3 3.1
We define the syntax of the simple representative procedural programming language While (defined and used for similar purposes in [5, 6]) with the following grammar (we use right-associative bracketing). Let X be a countably infinite set of variables. We let n range over values in N1, x over X, a over expressions of category AExp, b over expressions of category BExp, and p over expressions of category Prog. a ::= n | x | a + a | a ⋆ a | a − a b ::= ⊤ | ⊥ | a = a | a ≤ a | ¬b | b ∧ b p ::= x := a | skip | p; p | if b then p else p | while b do p We consider programs as expressions of category Prog. We denote the set of variables occurring in a program p with V ar(p), the set of subterms of p of category BExp with Bool(p), and the set of subterms of p of category AExp with Arith(p). Furthermore, with cl(p) we denote the smallest set of programs such that: – cl(p) is closed under subterms, i.e., if p1 ∈ cl(p), p2 ∈ Sub(p) and p2 ∈ Prog, then p2 ∈ cl(p); and – if while b do p1 ∈ cl(p), then also p1; while b do p1 ∈ cl(p) ∈ cl(p). 3.2
Given a finite subset of variables X ⊆ X, we define the set of states over X, denoted with StateX , as the set of total mappings µ : X → N.
We define the function BX that interprets expressions of category BExp as a function from StateX to B.
BX (s, a1 σ a2) = AX (s, a1) σ AX (s, a2) for σ ∈ {=, ≤}
BX (s, ¬b) = ¬BX (s, b)
BX (s, b1 ∧ b2) = BX (s, b1) ∧ BX (s, b2) We define the function AX that interprets expressions of category AExp as a function from StateX to N.
AX (s, n) = n for n ∈ N
AX (s, x) = state(x) for x ∈ X AX (s, a1 ρ a2) = AX (s, a1) ρ AX (s, a2) for ρ ∈ {+, ⋆} AX (s, a1 − a2) = AX (s, a1) − AX (s, a2) if AX (s, a1) − AX (s, a2) ≥ 0
AX (s, a1 − a2) = 0 if AX (s, a1) − AX (s, a2) < 0 For s ∈ StateX , x ∈ X and n ∈ N, we define s[x 7→ n](y) = n, if x = y, and s[x 7→ n](y) = s(y) if x 6= y.
For a program p and a set X such that var(p) ⊆ X ⊆ X, we define the operational semantics as follows. We consider the transition system (Γ, T, ⇒), where Γ = {(q, s) | q ∈ cl(p), s ∈ StateX }, T = StateX , and ⇒ ⊆ Γ × (Γ ∪ T ).
We define the relation ⇒ as the smallest relation such that for each s ∈ StateX , for each a ∈ AExp, and for each b ∈ BExp – we have (skip, s) ⇒ s; – we have (x := a, s) ⇒ s[x 7→ AX (a, s)]; – (p1, s) ⇒ (p′1, s′) implies (p1; p2, s) ⇒ (p′1; p2, s′); – (p1, s) ⇒ s′ implies (p1; p2, s) ⇒ (p2, s′);
1In this paper, we restrict ourselves to natural numbers, but the approach can be extended straightforwardly to other concrete domains. – we have (if b then p1 else p2, s) ⇒ (p1, s), if PX (b, s) = ⊤; – we have (if b then p1 else p2, s) ⇒ (p2, s), if PX (b, s) = ⊥; and – we have (while b do p, s) ⇒ (if b then (p; while b do p) else skip, s). Note that ⇒ is deterministic, i.e., for any s, t, t′, if s ⇒ t and s ⇒ t′, then t = t′. We say that p terminates on s with outcome t if (p, s) ⇒∗ t for t ∈ T . We say that p does not terminate on s if there is no t ∈ T such that (p, s) ⇒∗ t. We take notice of the fact that if p does not terminate on s, then there is an infinite sequence (p, s) ⇒ (p′, s′) ⇒ . . . starting from (p, s). 3.3
In order to simplify our encoding of While programs into the description logic ALC(D) later, we define a notion of normal forms for While programs. Consider the following substitutions, preserving the operational semantics of programs, for a fresh variable x, for ρ ∈ {+, ⋆, −}, and π ∈ {=, ≤}: ϕ[x := a1 ρ a2] ❀ x1 := a1 ; ϕ[x := x1 ρ a2] ϕ[x := a1 ρ a2] ❀ x2 := a2 ; ϕ[x := a1 ρ x2] ϕ[a1 π a2] ❀ x1 := a1 ; ϕ[x1 π a2] ϕ[a1 π a2] ❀ x2 := a2 ; ϕ[a1 π x2] p ❀ p; skip if a1 6∈ X if a2 6∈ X if a1 6∈ X if a2 6∈ X if p not of the form q; skip Using the transformations on programs given by the above substitutions, we can transform any program p to an operationally equivalent program p′ such that the following holds: – each subexpression of p′ of category AExp is either of the form x ρ y, for x, y ∈ X and ρ ∈ {+, ⋆, −}, or of the form n for n ∈ N; – for each subexpression of p′ of category BExp of the form t ρ s, for ρ ∈ {=, ≤}, holds t, s ∈ X; and – either p′ = skip, or p′ is of the form e; skip.
We will say that programs that satisfy this particular condition are in normal form. 4
We model programs in the language While using description logic and its modeltheoretic semantics. The concrete (i.e. numerical) values in the programming language correspond to concrete values in the description logic. States are represented by objects, and programs are represented by concepts. We represent the execution of programs on states by a (functional) role nextState. In particular, for a given program p with V ar(p) = {x1, . . . , xn}, we denote states s ∈ StateV ar(p) with objects that have concrete features valueOfxi .
An execution of a program p will then be modelled by means of a nextState sequence of objects. The objects in this sequence represent the states occurring in the particular execution of the program. Whenever in this execution of the program there occurs a state s such that the execution is continued from this state s with the intermediate program p′, the object corresponding to s is an element of the concept Cp′ . Also, whenever this execution terminates, the final object in this sequence is an element of the concept Cskip. 4.1
⊤ ⊑ ¬valueOfx↑
Cskip ⊑ ¬∃nextState.⊤ Take an arbitrary program p, i.e., an expression of category Prog. W.l.o.g., we assume p is in normal form. We define an ALC(D) TBox Tp as follows. We use concept names Cq for each q ∈ cl(p), and concept names Db for each b ∈ Bool(p).
For each variable x ∈ V ar(p), we create a concrete feature valueOfx, and we require We let nextState be an abstract feature and for Cskip we require: For each b ∈ Bool(p), we require the following, where x1, x2 range over X, and b1, b2 range over Bool(p):
Dx1=x2 ≡ ∃(valueOfx1 )(valueOfx2 ). = Dx1≤x2 ≡ ∃(valueOfx1 )(valueOfx2 ). ≤
D¬b1 ≡ ¬Db1
Db1∧b2 ≡ Db1 ⊓ Db2
Furthermore, we let D⊤ denote ⊤ and D⊥ denote ⊥. Then, for each q ∈ cl(p) of the
form p1; p2 we require the following for Cq, where p1, p2, q1, q2 range over cl(p), x, y1, y2
range over X, a ranges over Arith(p),
(
Cskip;p2 ⊑ Cp2 C(x:=n);p2 ⊑ ∃(nextState valueOfx). =n
C(x:=y);p2 ⊑ ∃(nextState valueOfx)(valueOfy). = C(x:=y1+y2);p2 ⊑ ∃(nextState valueOfx)(valueOfy1 )(valueOfy2 ).+ C(x:=y1−y2);p2 ⊑ (¬∃(valueOfy2 )(valueOfy1 ). ≤ ⊔ ∃(valueOfy1 )(nextState valueOfx)(valueOfy2 ).+) ⊓ (¬∃(valueOfy2 )(valueOfy1 ). > ⊔ ∃(nextState valueOfx). =0) C(x:=y1⋆y2);p2 ⊑ ∃(nextState valueOfx)(valueOfy1 )(valueOfy2 ).⋆
C(x:=a);p2 ⊑ ∃(valueOfy)(nextState valueOfy). = for y 6= x C(if b then q1 else q2);p2 ⊑ (¬Db ⊔ Cq1;p2 ) ⊓ (Db ⊔ Cq2;p2 )
C(while b do q);p2 ⊑ (¬Db ⊔ Cq;(while b do q);p2 ) ⊓ (Db ⊔ Cp2 )
Notice that, in general, the TBox Tp is not acyclic, since Axioms (
In order to use the above encoding of a program p into an ALC(D) TBox Tp to reduce
reasoning problems over programs into ALC(D) reasoning, we show the following
correspondence between the operational semantics of p and the model theoretic semantics
of Tp.
Lemma 1. For any program p, any X such that V ar(p) ⊆ X ⊆ X, any state s ∈
StateX , any b ∈ Bool(p), and for any model I = (∆ I, ·I) of Tp, we have that d ∈ ∆ I
and (d, s(xi)) ∈ valueOfIxi for all 1 ≤ i ≤ n implies that d ∈ CbI iff BX (b, s) = ⊤.
Proof (sketch). By induction on the structure of b. All cases follow directly from the
fact that Axioms (
Theorem 1. For any program p, any X such that V ar(p) ⊆ X ⊆ X, any state s ∈ StateX such that p terminates on s with outcome t, and for any model I = (∆ I, ·I) of Tp we have that d ∈ CpI and (d, s(xi)) ∈ valueOfIxi for all 1 ≤ i ≤ n implies that e ∈ Cskip and (e, t(xi)) ∈ valueOfIxi for all 1 ≤ i ≤ n, for some e ∈ ∆ I.
I I Proof. By induction on the length of the ⇒-derivation (p, s) ⇒k t. Assume d ∈ Cp and (d, s(xi)) ∈ valueOfIxi for all 1 ≤ i ≤ n, for some d ∈ ∆ I. The base case k = 0 holds vacuously. In the case for k = 1, we know p = skip, since p is in normal form. Therefore, we know s = t, and thus e = d witnesses the implication.
In the inductive case, we distinguish several cases. Case p = skip; q. We know I (p, s) ⇒ (q, s) ⇒k−1 t. Since I satisfies Tp, by Axiom (8), we know d ∈ Cq . The result now follows directly by the induction hypothesis.
Case p = (x := a); q. We know (p, s) ⇒ (q, s′) ⇒k−1 t, and s′ = s[x 7→ AX (a, s)].
Since I satisfies Tp, by Axioms (
Case p = (if b then p1 else p2); q. Assume BX (b, s) = ⊤. Then (p, s) ⇒ (p1; q, s) ⇒k−1
I t. By Lemma 1, we know d ∈ Db. Then, by the fact that Axiom (15) holds, we know
I d ∈ Cp1;q. The result now follows directly by the induction hypothesis. For BX (b, s) = ⊥ an analogous argument holds.
Case p = (while b do p1); q. Assume BX (b, s) = ⊤. Then (p, s) ⇒2 (p1; p, s) ⇒k−2
I t. By Lemma 1, we know d ∈ Db. Then, by the fact that Axiom (16) holds, we know d ∈ Cp1;p. The result now follows directly by the induction hypothesis.
If, however, in the same case holds BX (b, s) = ⊥, then (p, s) ⇒3 (q, s) ⇒k−3 t. By
I I Lemma 1, we know d 6∈ Db. By the fact that Axiom (16) holds, we know d ∈ Cq . The result now follows directly by the induction hypothesis.
Theorem 2. For any program p, any X such that V ar(p) ⊆ X ⊆ X any state {x1 7→ c1, . . . , xn 7→ cn} = s ∈ StateX such that p does not terminate on s, there exists a model I = (∆ I, ·I) of Tp such that for some d ∈ ∆ I we have d ∈ CpI, (d, ci) ∈ valueOfIxi ,
I for all 1 ≤ i ≤ n, and Cskip = ∅.
Proof. Since p does not terminate on s, we know there exists an infinite ⇒-sequence (pi, si) ⇒ (pi+1, si+1), for i ∈ N, where (p1, s1) = (p, s). Consider the following interpretation I = (∆ I, ·I), where ∆ I N}. For q ∈ cl(p), we let CqI = {(pi, si) | pi = q}. For b ∈ Bool(p=), w{e(plie,tsiD) bI| =i {∈(pi, si) | i ∈ N, PX (b, s) = ⊤}. For each x ∈ X, we let valueOfIx = {((pi, si), si(x)) | i ∈ N}. We let nextStateI = {((pi, si), (pi+1, si+1)) | i ∈ N}.
I I
The definition of I implies that Cskip = ∅. Assume (pk, sk) ∈ Cskip. Then pk = skip, and thus (pk, sk) ⇒ sk, which contradicts our assumption of non-termination.
I
Clearly, I satisfies Axiom (
To see that I satisfies Axioms (
I the interpretation an arbitrary class Cq , and we distinguish several cases. Consider pj = skip; q. Then by the constraints on ⇒, pj+1 = q and sj+1 = sj. This witnesses that the subsumption in Axiom (8) holds.
Consider pj = (x := a); q. Then by the constraints on ⇒, pj+1 = q and sj+1 =
sj[x 7→ AX (a, sj)]. By definition of I, we know ((pj, sj), (pj+1, sj+1)) ∈ nextStateI. It is
now easy to verify that the subsumptions in Axioms (
Consider pj = (if b then p′1 else p′2); q. Assume BX (b, sj) = ⊤. Then (pj, sj) ∈ Db. Also, by the constraints on ⇒, pj+1 = p′1; q and sj+1 = sj. It is easy to verify that, in this case, the subsumption in Axiom (15) holds. The case for BX (b, sj) = ⊥ is completely analogous.
Consider pj = (while b do p′); q. If BX (b, sj) = ⊤, then (pj, sj) ∈ DbI and pj+1 = p′; pj and sj+1 = sj. If BX (b, sj) = ⊥, then (pj, sj) 6∈ DbI and pj+1 = skip; q and sj+1 = sj. It is easy to verify that, in either case, the subsumption in Axiom (16) holds.
Theorem 3. For any program p, any X such that V ar(p) ⊆ X ⊆ X any state {x1 7→ c1, . . . , xn 7→ cn} = s ∈ StateX such that p terminate on s, there exists a model I = (∆ I, ·I) of Tp such that for some d ∈ ∆ I we have d ∈ CpI, (d, ci) ∈ valueOfIxi , for all 1 ≤ i ≤ n.
Proof (Sketch). We know there exists (p, s) ⇒k (p′, s′) ⇒ t. Analogously to the proof of Theorem 2, we can construct a model I from the sequence (p, s) ⇒k (p′, s′). By similar arguments to those in the proof of Theorem 2 it follows that I |= Tp. Then, (p, s) ∈ CpI witnesses the further constraints on I.
Note that the syntax and operational semantics of While can be adapted to various concrete domains with varying operators. The encoding into ALC(D) can be adapted correspondingly, and a corresponding correlation between the operational semantics and the model theoretic semantics can be proven. 4.3
To illustrate the method described above, of encoding While programs into ALC(D) TBoxes, we will consider an example. Let p0 be the following program in normal form, that computes the factorial of the value stored in variable x and outputs this in variable y. Note that variable z is simply used to refer to the constant value 1. p0 =
(y := 1; z := 1; while x > z do (y := y ⋆ x; x := x − z); skip) Furthermore, we will use the following abbreviations to refer to subprograms of p0. p1 = (z := 1; while x > z do (y := y ⋆ x; x := x − z); skip) p2 = (while x > z do (y := y ⋆ x; x := x − z); skip) p3 = (y := y ⋆ x; x := x − z) p4 = (x := x − z) We can now construct the ALC(D) TBox Tp0 , in the fashion described above. Note that Tp0 is not acyclic, since there are inclusion axioms (a) with Cp2 as lhs and Cp3;p2 in the rhs, (b) with Cp3;p2 as lhs and Cp4;p2 in the rhs, and (c) with Cp4;p2 as lhs and Cp2 in the rhs. These axioms are marked with the symbol †.
It is straightforward to construct models of the TBox Tp0 . One can simply take an execution of the program p0, and transform this execution into a model of Tp0 according to the intuition behind the encoding described above. 5
Theorems 1, 2 and 3 allow us to use the encoding of While programs into ALC(D) to reduce several reasoning problems over While programs to reasoning problems over ALC(D). For instance, termination of a program p reduces to unsatisfiability of the ABox Ap = {o1 : Cp} with respect to the TBox Tp ∪ {Cskip ⊑ ⊥}.
Also, we are able to encode abduction problems over While problems in the description logic ALCO(D), which is ALC(D) extended with nominals. The question what input states for a program p could have led to the (partial) output state s, for dom(s) ⊆ V ar(p), reduces to finding models for Ap = {i : Cp, o : Cskip} ∪ {(o, s(x)) : valueOfx | x ∈ dom(s)} and Tp, where Cskip is required to be a nominal concept.
Another example is checking whether two (terminating) programs p1 and p2 are equivalent. Without loss of generality, we can assume V ar(p1) = V ar(p2). This equivalence check can be reduced to the problem of ALCO(D) unsatisfiability of the ABox Ap1,p2 = {o : Cp1 , o : Cp2 , s : Ctest} with respect to the TBox Sp1 ∪Sp2 ∪Teq, where Spi is Tpi with Cskip replaced by Cskip, and Teq = {Ctest ≡ (∃.(res1 valueOfx1 )(res2 valueOfx1 ). 6= i ⊔ · · · ⊔ ∃.(res1 valueOfxn ) (res2 valueOfxn ). 6=) ⊓ ∃res1.Cs1kip ⊓ ∃res2.Cs2kip}, for res1, res2 abstract features, and Cs1kip, Cs2kip and Ctest nominal concepts.
Naturally, this approach allows us to encode more intricate reasoning problems over While programs into description logic reasoning problems. Description logic offers us a very flexible formalism to express a variety of reasoning problems over While programs. 5.1
A bit of care has to be taken with this powerful and general approach. The problems we consider generally balance on the bounds of decidability.
A concrete domain D is called arithmetic if its values contain the natural numbers, and it contains predicates for equality, equality with zero and incrementation. Unfortunately, satisfiability of ALC(D) concepts for arithmetic concrete domains D with respect to general TBoxes is undecidable [4]. So, for many cases, our approach doesn’t directly result in a decision procedure.
This is no surprise, however. We know that we cannot decide equivalence of While programs in general. For instance for the concrete domain Z (with addition and equality) we can easily encode the undecidable problem of whether a given Diophantine equation Φ(x1, . . . , xn) = 0 has an integer solution (the subject of Hilbert’s Tenth Problem) as a reasoning problem over While programs. Similarly, it can be proven that equivalence of While programs with concrete domain N is undecidable.
Nevertheless, several decidable fragments of the While language can be obtained by either restricting the concrete domains or by forbidding statements of the form (while b do p). By forbidding these while-statements, we end up with acyclic TBoxes. We know that reasoning with respect to acyclic TBoxes is decidable for ALC(D). Restricting the concrete domain (and keeping while-statements), does not change the fact that we are dealing with general TBoxes. In this case, the concrete domain needs to be restricted quite severely, to get decidability. 5.2
We can use the example from Section 4.3 to illustrate how to encode several reasoning problems over While programs into ALC(D) reasoning problems. For instance, we can encode the problem of checking whether p0 is terminating as the unsatisfiability problem of the ABox {o1 : Cp0 } with respect to the TBox Tp ∪ {Cskip ⊑ ⊥}.
Using the expressivity of the description logic ALC(D), we can in fact express a variety of different semantic properties to be checked automatically. For instance, in this fashion, we can express the problem whether p0 does not terminate with an output value for y that is less than or equal to 20 for all input values for x that are greater than or equal to 4. This problem can be reduced to the unsatisfiability of the ABox {o1 : Cp0 ⊓∃(hasValuex). ≥4} with respect to the TBox Tp∪{Cskip ⊑ ∃(hasValuey). ≤20}.
These examples of expressing reasoning problems in the ALC(D) language illustrate the flexibility we get in expressing different reasoning problems. We can reduce the decision of any semantic property of While programs that is expressible using the modelling of While programs in the ALC(D) language to reasoning on ALC(D).
The results presented in this paper are only the beginning of a larger inquiry investigating the possibilities and bounds of approaching automated reasoning over (procedural) programming languages by means of assigning model-theoretic semantics to programs. We suggest a number of directions for further research needed to get a better understanding of the topic.
Similar encodings of programming languages into the description logic ALC(D) could also be devised also for other procedural programming languages, as well as for declarative programming languages. It needs to be investigated to what extent this method is extendable to such other languages. Suitable programming languages for which this could be investigated as a next step include extensions of the programming language While with language constructs for nondeterminism or parallellism, procedural programming languages that are based on goto-statements rather than whilestatements, and simple, representative functional and logic programming languages that operate on similar domains (e.g. numerical values). Once the method presented in this paper has been applied to such languages, it will also be possible to investigate to what extent reasoning problems on multiple programs of different programming languages (e.g. the equivalence problem of a While program and a program of a goto-based language) can be encoded in this framework.
Another important direction for further research is identifying larger fragments of the programming language While for which reasoning problems on programs such as the ones we considered in this paper are decidable. By encoding programs into description logics, we get a conceptually simpler setting to investigate such questions. Programming languages can have a variety of different constructs behaving in various ways. Reasoning over such diverse structures can get rather messy and complex. On the other hand, practically all reasoning problems for description logics can be reduced to finding models for description logic knowledge bases (i.e. reduced to the satisfiability problem). The problem of finding such models is conceptually simple, and the semantic definition of the description logic language guides the search for models. Such a conceptually simpler setting might make it easier to identify decidable fragments. In addition to this conceptual simplification of the problem, we could use results and techniques from the field of description logic when investigating the decidability of such fragments. For those fragments of the programming languages that lead to decidable reasoning problems, we can investigate the computational complexity of these reasoning problems. 7
We assigned a model theoretic semantics to programs of the simple procedural language While, by encoding them into the description logic ALC(D). This allowed us to express a variety of reasoning problems over While programs using the expressivity of the description logic ALC(D). Furthermore, for a number of restricted fragments of the programming language While, this directly results in a method of solving such reasoning problems using existing (description logic) algorithms. Furthermore, this encoding leads to a new approach of exploring what fragments of the programming language allow for decidable reasoning over programs. Further research includes a further characterization of fragments of the language that allow decidable reasoning, and extending this approach to different procedural (and declarative) programming languages.