Filesystemlar haqida hech o'ylab ko'rganmisiz masalan fs hierarchy.
/
/root
/home
/home/user

Algorithmchilar biladi bu narsa oddiy tree. Ammo sizga algorithmlar ham yordam berolmaydi bazi caselarda.

Masalan oddiy edge case bor. / ni parenti yo'q.

Ho'sh siz qilyotgan structure, algorithmlar qnachalik tog'ri ekanini qanday tekshirish mumkin ?

Testlar ?
Xop biz qilgan fs treedagi barcha caselarni cover qilib ko'ringchi.

Manda boshqa ideya bor, agar testlarni aqli yetmaydigan bo'lsa demak boshqa narsa qilish mumkin.

Specifications

Hullas ideya bunday biz oldin spesifikatsiya yozamiz. Yani tizimni invariantlari va cheklovlarini tariflaymiz va qandaydir tool yani aynan shu specni check qiladigan tool barcha holatlarni analiz qilib biz qilgan modeldagi muammolarni ko'rsatadi.

Masalan Alloy6

sig Dir extends FSObject {}
sig File extends FSObject {}

abstract sig FSObject {
  parent: lone Dir 
}

sig Root extends Dir {} {
  no parent
}

fact NoCycle {
  no d: Dir | d in d.^(~parent)
}

Endi buni tushunishga xarakat qilamiz. Undan oldin keling specni mantiqiy darajada o'ylab olaylik biz oddiy directory uchun model qilamiz.

1. FSObject - Bu file yoki directory bo'lishi mumkin xozir bizni holatda faqat directory. Ammo FS objectda rule bor. Ko'pi bilan bitta parent dir. Mantiqiy jixatdan bitta directoryda 2ta parent bo'lmaydiku ahir ))

2. Root - eng top leveldagi directory / Bu yerda yana rule yani uning parenti yo'q.

Mana bizda qandaydir objectlar va ularga nisbatan mantiqiy qoidalar paydo bo'ldi. Endi yana bir mantiqiy qismi qoldi. Ammo buni biz fakt deymiz. Bu qoida emas yani talab emas bu aniq fakt!

Fakt quyidagicha: Hech bir directory o'zining ajdodi bo'la olmaydi

Etibor qilgan bo'lsangiz biz mantiqga asoslangan spesifikatsiya yozdik. Alloy6 esa manashu specni o'zi tekshiradi va bizni mantiqdagi xatoliklarni ko'rsatishi mumkin.