Semantik: attribute grammar ve weakest precondition

Sözdizimi (syntax) bir programın biçimini tanımlar; ama “değişken kullanılmadan önce bildirilmeli” ya da “int’e real atanamaz” gibi kurallar BNF ile yazılamaz. Bu sayfa iki şeyi kapsar: bu kuralları yazmak için attribute grammar ve programın anlamını (semantics) tanımlamak için üç yöntem. Sınavda en sık çıkan iki soru tipi: attribute grammar ile tip kontrolü yapmak ve weakest precondition hesaplamak.

Altın kurallar:

1. Synthesized yukarı, inherited aşağı akar.
2. Önce look-up, sonra expected_type, sonra actual_type, en son predicate.
3. Weakest precondition sondan başa hesaplanır. Postcondition’daki değişkenin yerine atamanın sağ tarafını yaz.
4. Negatif sayıyla bölünce eşitsizlik yön değiştirir.

Static semantics

Bazı kurallar derleme zamanında kontrol edilir ama context-free grammar ile ifade edilemez ya da edilmesi çok zahmetlidir:

• Java’da float bir değer int değişkene atanamaz.
• Tüm değişkenler kullanılmadan önce bildirilmeli.
• Ada’da bir alt programın sonundaki end adı, başındaki adla aynı olmalı.

Bunlara static semantics denir: anlamla ilgili ama çalıştırmadan, derleme zamanında kontrol edilebilen kurallar. Adı “semantics” olsa da aslında sözdizimine yakındır.

Attribute grammar

Attribute grammar, bir CFG’ye üç şey ekler:

• Attribute’lar: her sembole bağlı değerler (actual_type, expected_type).
• Semantic function’lar (attribute computation functions): her kurala bağlı, attribute’ların nasıl hesaplandığını söyleyen kurallar.
• Predicate’ler: kuralın geçerli olması için doğru olması gereken koşullar. Biri false olursa static semantics hatası var.

Üç tür attribute var:

Tip kontrolü örneği

1. <assign> -> <var> = <expr>
   <expr>.expected_type <- <var>.actual_type
2. <expr> -> <var>[2] + <var>[3]
   <expr>.actual_type <- if (<var>[2].actual_type = int) and
                            (<var>[3].actual_type = int) then int else real
   predicate: <expr>.actual_type == <expr>.expected_type
3. <expr> -> <var>
   <expr>.actual_type <- <var>.actual_type
   predicate: <expr>.actual_type == <expr>.expected_type
4. <var> -> A | B | C
   <var>.actual_type <- look-up(<var>.string)

Köşeli parantezli indisler (<var>[2]) aynı nonterminal’in farklı örneklerini ayırır. A = B + C için A real, B real, C int olsun:

adım                                   değer
1. <var>.actual_type <- look-up(A)     real      (intrinsic)
2. <expr>.expected_type <- real        real      (inherited)
3. <var>[2] = look-up(B), <var>[3]     real, int (intrinsic)
4. <expr>.actual_type                  real      (synthesized: ikisi de int değil)
5. predicate real == real              TRUE

A int, B int, C real olsaydı: expected int, actual real, predicate false. Bu gramer otomatik dönüşüm (coercion) yapmaz; A real, B int, C int bile hata verir çünkü actual int, expected real.

Bağlamdan bağımsız olmayan dil

$a^n b^n c^n$ dili CFG ile yazılamaz. Attribute grammar ile kolay:

<S> -> <A> <B> <C>      predicate: <A>.size == <B>.size == <C>.size
<A> -> a | <A>[2] a     <A>.size <- 1  |  <A>.size <- <A>[2].size + 1
(B ve C için aynı)

CFG kısmı a+b+c+ biçimini kabul eder. aabbcc geçer; aabbc sözdizimsel olarak doğru ama predicate false.

Dinamik semantik: üç yöntem

Operational semantics

Yüksek seviyeli bir yapının anlamını, daha basit ve iyi bilinen bir dile çevirerek verir. C’nin for döngüsü:

for (expr1; expr2; expr3) { ... }

        expr1;
loop:   if expr2 == 0 goto out
        ...
        expr3;
        goto loop
out:    ...

Okuyan biri for’u bilmese de if ve goto’yu biliyorsa anlamı çözer.

Denotational semantics

Her sözdizimsel yapı için bir matematiksel fonksiyon tanımlanır. İkili sayı örneği:

M_bin('0') = 0
M_bin('1') = 1
M_bin(<bin_num> '0') = 2 * M_bin(<bin_num>)
M_bin(<bin_num> '1') = 2 * M_bin(<bin_num>) + 1

101 için: ‘1’ → 1, ‘10’ → 2, ‘101’ → 5. 10110 için 22. Programlarda durum (state) değişkenlerin değerlerinden oluşur; her ifade bir durumdan başka bir duruma giden fonksiyondur.

Axiomatic semantics

Bir ifade S için şu üçlüye Hoare triple denir:

$\{P\}\; S \;\{Q\}$

P precondition (önkoşul), Q postcondition (sonkoşul). Anlamı: S çalışmadan önce P doğruysa, S bittiğinde Q doğrudur. Q verildiğinde, Q’yu garanti eden en az kısıtlayıcı önkoşula weakest precondition denir.

Atama aksiyomu

$x = E$ ataması ve postcondition Q için:

$wp(x = E,\ Q) = Q_{x \to E}$

Q’daki her x yerine E yaz, sadeleştir. Örnek: x = 2 * y - 3 {x > 7}:

$2y - 3 > 7 \;\Rightarrow\; 2y > 10 \;\Rightarrow\; y > 5$

Kontrol etmeyi alışkanlık yap: y = 6 → x = 9 > 7 doğru; y = 5 → x = 7, 7 > 7 yanlış. Sınır doğru dışlanmış.

TUZAK · negatif katsayı. a = -2 * b + 4 {a < 0}: $-2b + 4 < 0 \Rightarrow -2b < -4 \Rightarrow b > 2$. Eşitsizliğin iki tarafını -2’ye bölünce yön döner. b < 2 yazan yanar. Bir değer deneyerek kontrol et: b = 3 → a = -2 < 0, doğru.

Sıralı ifadeler

$S_1;\ S_2$ için önce $S_2$‘nin weakest precondition’ını bul, o $S_1$‘in postcondition’ı olur:

y = x + 4;
x = y * 2;
{x < 20}

adım 1 (son atama):  2y < 20      →  y < 10
adım 2 (ilk atama):  x + 4 < 10   →  x < 6
sonuç: {x < 6}

Seçim

if B then S1 else S2 için:

$wp = (B \wedge wp(S_1, Q)) \vee (\neg B \wedge wp(S_2, Q))$

if (x > 0) y = x - 1; else y = x + 1; {y > 0}: then dalı x > 1 verir (x > 0 ile birleşince yine x > 1). Else dalı x > -1 verir; x ≤ 0 ile birleşince tam sayılarda sadece x = 0. Cevap: x > 1 veya x = 0.

Daha güçlü önkoşul da geçerli

{x > 5} x = x - 3 {x > 0} geçerli bir üçlüdür, ama weakest değil. Weakest x > 3. Rule of consequence: P’ ⇒ P ise ve {P} S {Q} geçerliyse, {P’} S {Q} de geçerlidir. Yani weakest precondition’dan daha güçlü her önkoşul işe yarar; daha zayıfı yaramaz (x ≥ 3 için x = 3 → 0 > 0 yanlış).

Döngüler

while B do S için weakest precondition doğrudan hesaplanamaz; bir loop invariant (döngü değişmezi) I bulmak gerekir. I döngüden önce doğru olmalı, her turdan sonra da doğru kalmalı ve döngü bittiğinde ($I \wedge \neg B$) Q’yu gerektirmeli. Invariant bulmak tümevarıma benzer ve genelde vizede yüzeysel sorulur: “invariant nedir, hangi üç koşulu sağlamalı?”

Sık yapılan hatalar

1. <assign> -> <var> = <expr>
   <expr>.expected_type <- <var>.actual_type
2. <expr> -> <var>[2] + <var>[3]
   <expr>.actual_type <- if (<var>[2].actual_type = int) and
                            (<var>[3].actual_type = int) then int else real
   predicate: <expr>.actual_type == <expr>.expected_type
3. <expr> -> <var>
   <expr>.actual_type <- <var>.actual_type
   predicate: <expr>.actual_type == <expr>.expected_type
4. <var> -> A | B | C
   <var>.actual_type <- look-up(<var>.string)

M_bin('0') = 0
M_bin('1') = 1
M_bin(<bin_num> '0') = 2 * M_bin(<bin_num>)
M_bin(<bin_num> '1') = 2 * M_bin(<bin_num>) + 1