1
ðc tZ (5)
Nguyn Thanh Bình
Khoa Công nghThôngtin
Trưng ði hc Bách khoa
ði hc ðà Nng
2
Gii thiu
ñưc ñ xut bi Jean René Abrial ði hc
Oxford
ngôn ngñc thình thc ñưc sdng rng rãi
nht
da trên lý thuyt tp hp
ký hiu toán hc
sdng các sơ ñ (schema)
dhiu
2
3
Gii thiu
Gm bn thành phn cơ bn
các kiu dliu (types)
•da trên khái nim tp hp
các sơ ñ trng thái (state schemas)
•mô tcác bin và ràng buc trên các bin
các sơ ñ thao tác (operation schemas)
•mô tcác thao tác (thay ñi trng thái)
các toán tsơñ (schema operations)
•ñnh nghĩa các sơ ñ mi t!các sơ ññãcó
4
Kiu dliu
m$i kiu dliu là mt tp hpcác phn t
Ví d
{true, false} : kiu lô-gíc
N: kiu stnhiên
Z: kiu snguyên
R: kiu sthc
{red, blue, green}
3
5
Kiu dliu
Các phép toán trên tp hp
Hi: A ∪B
Giao: A ∩B
Hiu: A ⁄B
Tp con: A ⊆B
Tp các tp con: P A
•ví d: P {a, b} = {{}, {a}, {b}, {a, b}}
6
Kiu dliu
mt skiu dliu cơ bn ñã ñưc ñnh
nghĩa trưc
kiu snguyên Z
kiu stnhiên N
kiu sthc R
...
có thñnh nghĩa các kiu dliu mi
ANSWER == yes | no
[PERSON]
•sdng cp ký hiu [ và]ññnh nghĩa kiu cơ
bn mi
4
7
Kiu dliu
Khai báo kiu
x : T
•x là phn tc&a tp T
Ví d
•x : R
•n : N
•3 : N
•red : {red, blue, green}
8
Vt!
Mt vt!(predicate)ñưc sdng ññnh
nghĩa các tính cht c&a bin/giá tr
Ví d
x > 0
π ∈ R
5
9
Vt!
Có thsdng các toán tlô-gíc ññnh nghĩa các v
t!phc tp
Và: A
∧
B
Hoc: A
∨
B
Ph&ñnh:
¬
A
Kéo theo: A
⇒
B
Ví d
(x > y)
∧
(y > 0)
(x > 10)
∨
(x = 1)
(x > 0) )
⇒
x/x = 1
(
¬
(x
∈
S))
∨
(x
∈
T)
10
Vt!
Các toán tkhác
(∀x : T •A)
•A ñúng vi mix thuc T
•Ví d: (∀x : N •x - x =0)
(∃x : T •A)
•A ñúng vi mt sgiá trx thuc T
•Ví d: (∃x : R •x + x = 4)
{x : T | A}
•biu din các phn tx c&a T th(a mãn A
•Ví d: N = {x : Z | x ≥0}