Bosh sahifa Wiki Semantics

Semantics

Semanticsdasturlash tilidagi syntactically to‘g‘ri konstruksiyalarning ma’nosi va bajarilish xatti-harakatini belgilaydigan qoidalar.

Syntax kod qanday yozilishini, semantics esa u nimani anglatishini tushuntiradi.

Masalan:

a + b

syntax jihatdan qo‘shish ifodasi. Semantikasi a va b type’iga qarab sonlarni qo‘shish, stringlarni birlashtirish yoki operator overloadni chaqirish bo‘lishi mumkin.

Static semantics

Compile vaqtida tekshiriladigan ma’no qoidalari static semantics deb ataladi.

Misollar:

Kod grammatik jihatdan to‘g‘ri bo‘lsa ham static semantic xato berishi mumkin.

integer x = "text"

syntax to‘g‘ri, type semantikasi noto‘g‘ri.

Dynamic semantics

Dastur bajarilganda qanday holat o‘zgarishi dynamic semantics bilan belgilanadi.

Masalan:

  • assignment xotiradagi qiymatni o‘zgartiradi;
  • function call yangi stack frame yaratadi;
  • exception control flowni o‘zgartiradi;
  • await coroutine’ni to‘xtatadi;
  • object allocation heap’dan joy oladi.

Runtime xatolari dynamic semantikaga bog‘liq.

Operational semantics

Til konstruksiyasi abstrakt machine yoki bosqichlar orqali qanday bajarilishini tasvirlaydi.

Masalan, assignment:

  1. o‘ng ifoda hisoblanadi;
  2. target manzil topiladi;
  3. qiymat conversion qilinadi;
  4. xotiraga yoziladi.

Small-step semantics har kichik qadamni, big-step semantics esa ifodadan yakuniy natijaga o‘tishni ko‘rsatadi.

Denotational semantics

Har til konstruksiyasini matematik obyekt yoki funksiya bilan bog‘laydi.

Masalan, expression environmentdan qiymatga mapping sifatida qaraladi.

Bu til xususiyatlarini formal isbotlashda ishlatiladi.

Axiomatic semantics

Dastur xatti-harakati precondition va postcondition orqali ifodalanadi.

Hoare triple:

{P} C {Q}

Bu yerda:

  • P — oldingi shart;
  • C — command;
  • Q — keyingi shart.

Program verification va design by contract bilan bog‘liq.

Evaluation order

Ifodadagi operandlar qaysi tartibda hisoblanishi semantics qismidir.

f() + g()

Til:

  • chapdan o‘ngga;
  • o‘ngdan chapga;
  • unspecified

tartib berishi mumkin.

Agar functionlar side effect qilsa, tartib natijaga ta’sir qiladi.

Short-circuit

Boolean operatorlar ikkinchi operandni shartga qarab bajarmasligi mumkin.

user != null && user.active

Birinchi shart false bo‘lsa ikkinchi qism bajarilmaydi.

Bu null accessdan himoya va performance uchun ishlatiladi.

Value va reference semantics

Value semantics’da assignment qiymat nusxasini beradi.

Reference semantics’da ikki variable bir objectga qarashi mumkin.

b = a

dan keyin b orqali o‘zgarish ada ko‘rinishi yoki ko‘rinmasligi type modeliga bog‘liq.

Equality semantics

== operatori:

  • qiymat tengligi;
  • object identity;
  • reference tengligi;
  • overloaded comparison

ma’nosida ishlatilishi mumkin.

Hash-based collection uchun equality va hash contracti mos bo‘lishi kerak.

Integer overflow

Fixed-width integer diapazondan chiqsa til:

  • wrap;
  • exception;
  • undefined behavior;
  • saturate;
  • compile-time error

qoidalaridan birini qo‘llashi mumkin.

Bir xil syntax boshqa tilda boshqa natija beradi.

Undefined behavior

Specification ayrim holat uchun hech qanday talab bermasa undefined behavior.

Compiler bunday holat sodir bo‘lmaydi deb optimization qilishi mumkin.

Misollar ayrim tillarda:

  • signed overflow;
  • invalid pointer;
  • data race;
  • out-of-bounds.

Undefined behavior shunchaki “tasodifiy xato” emas; programning barcha natijasi ishonchsiz bo‘lishi mumkin.

Unspecified behavior

Specification bir nechta ruxsat etilgan variant beradi, implementation qaysi birini tanlashini hujjatlashtirishi shart emas.

Bu undefined behaviordan farqli: natijalar chegaralangan.

Implementation-defined behavior

Implementation variantni tanlaydi va hujjatlashtiradi.

Masalan:

  • type hajmi;
  • signed right shift;
  • character encoding;
  • endianness.

Portable kod implementation hujjatini hisobga oladi.

Side effect

Ifoda tashqi holatni o‘zgartirsa side effect mavjud.

Misollar:

Pure function side effectsiz bo‘lib, bir xil input uchun bir xil natija beradi.

Memory model

Concurrent programda write boshqa threadga qachon ko‘rinishi semantics bilan belgilanadi.

Memory model:

  • atomicity;
  • ordering;
  • data race;
  • happens-before;
  • synchronization

qoidalarini beradi.

Faqat source tartibi CPU bajarilish tartibini kafolatlamaydi.

Exception semantics

Til exception:

  • qayerda ushlanadi;
  • stack qanday ochiladi;
  • cleanup bajariladimi;
  • finally tartibi;
  • async exception

qoidalarini belgilaydi.

Destructor yoki resource cleanup semantikasi xatoda muhim.

Type coercion

Turli type operandlar avtomatik conversion qilinishi mumkin.

integer + float

integer floatga o‘tishi mumkin.

String va son conversion qoidalari noaniq bo‘lsa kutilmagan natija beradi.

Semantic version o‘zgarishi

Til yoki library yangi versiyada syntaxni saqlab, ma’noni o‘zgartirsa semantic breaking change yuz beradi.

Masalan, default sorting, timeout yoki equality xatti-harakati o‘zgarishi consumer code’ni buzishi mumkin.

Compatibility faqat compile bo‘lish bilan o‘lchanmaydi.

Formal specification

Til specificationi semanticsni:

orqali belgilaydi.

Implementationlar bir xil specificationga mos bo‘lishga intiladi.

Observational equivalence

Ikki implementation tashqi kuzatuvchi uchun bir xil natija va side effect bersa, ma’lum contract doirasida semantik ekvivalent hisoblanishi mumkin. Compiler optimization eski kodni yangi ko‘rinishga o‘zgartirganda shu xususiyatni saqlashi kerak.

Aliasing

Ikki reference bir xil object yoki memory hududiga qarashi mumkin. Bir yo‘l orqali yozuv boshqasida ko‘rinadi. Aliasing optimization, mutability va thread safety semantikasini murakkablashtiradi.

Determinism

Bir xil input va boshlang‘ich holat uchun doim bir xil natija beradigan amal deterministic. Thread scheduling, random manba, vaqt va tashqi service nondeterminism kiritishi mumkin. Test va distributed protocol bu manbalarni explicit boshqaradi.

Bog‘liq tushunchalar

Syntax, Static semantics, Dynamic semantics, Type system, Evaluation order, Undefined behavior, Side effect, Memory model, Formal verification