Nguyên lý và phương pháp lp trình
Kim chng tính ñúng ñn ca
chương trình
TS. Nguy$n Tu%n ðăng
1
Ni dung
•Lp trình có c%u trúc
•Các phương pháp hình thc
•Lp trình có c%u trúc theo ti-p cn top-down
•Cách ti-p cn k-t h/p
•
Cá
c
c
%
u
trú
c
nh
t
0
(sequences)
•
Cá
c
c
%
u
trú
c
nh
t
0
(sequences)
–Các c%u trúc trình t0 – hình thc hóa
–Các c%u trúc trình t0 – kim chng
–Các c%u trúc trình t0 – sơ ñ2 kim chng
•Các c%u trúc ñi3u ki4n
–Các c%u trúc ñi3u ki4n – hình thc hóa
–Các c%u trúc ñi3u ki4n – kim chng
–Các c%u trúc ñi3u ki4n – sơ ñ2 kim chng 2
Ni dung (tt)
•Các c%u trúc vòng l6p
–Các c%u trúc vòng l6p – ví d8
–Các c%u trúc vòng l6p – chương trình d9n xu%t
–Các c%u trúc vòng l6p – k-t qu<
–Các c%u trúc vòng l6p – sơ ñ2 kim chng
–
Cá
c
c
%
u
trú
c
vò
ng
l
6
p
–
cá
c
l
=
i
trong
ki
m
ch
ng
–
Cá
c
c
%
u
trú
c
vò
ng
l
6
p
–
cá
c
l
=
i
trong
ki
m
ch
ng
•Tóm lư/c
3
Lp trình có cu trúc
•Chương trình s> d8ng các c%u trúc ñi3u khin căn
b<n theo nguyên tc 1-in, 1-out :
–C%u trúc trình t0 :begin S1 S2 end
–C%u trúc ch@n l0a : if Ethen S1 else S2 end
–
C
%
u
trú
c
vò
ng
l
6
p
:
while
E
loop
S
1
end
–
C
%
u
trú
c
vò
ng
l
6
p
:
while
E
loop
S
1
end
–Các c%u trúc ñi3u khin trên còn bao g2m thêm : if vAi
elseif,case,for, etc.
•Boehm và Jacopini, 1966
–Chng minh rCng c%u trúc ñi3u khin ca b%t kỳ mEt
lư/c ñ2 chương trình nào cũng có th ñư/c biu ñGt mà
không cIn dùng các phát biu gotos, chL cIn dùng các
c%u trúc: trình t0, ch@n l0a và vòng l6p.
4
Lp trình có cu trúc
• Edsger Dijkstra, 1970
–Lý lun rCng các phát biu goto là có hGi trong chương
trình, ñ2ng thNi ñưa ra ý tưOng v3 vi4c kim chng tính
ñúng ñn ca chương trình bCng các phương pháp hình
thc.
5