EWIDENCJA MANDATÓW KREDYTOWYCH
Typy bazowe
[NUMER_STRAŻNIKA, NAZWISKO, IMIE, NUMER_BLOCZKU, ILOŚĆ_ODCINKÓW_W_BLOCZKU, DATA, ILOŚĆ_ODCINKÓW_NIEWYKORZYSTANYCH, NUMER_ODCINKA, KWOTA MANDATU, PESEL, SYMBOL_DOKUMENTU_TOZSAMOSCI, NAZWA_DOKUMENTU_TOZSAMOŚCI, NUMER_DOKUMENTU_TOZSAMOSCI, ADRES]
[ODDANY = {„tak”, „nie}]
[KOMUNIKAT =
{
„Strażnik o takim numerze już istnieje”,
„Nie ma takiego strażnika”,
„Taki bloczek już wydano”,
„Data pobrania późniejsza niż dzisiaj”,
„Nie wydano takiego bloczku”,
„Ten bloczek już zwrócono”,
„Data zwrotu wcześniejsza od daty wydania”,
„Bloczek zwracany przez nieistniejącego straznika”,
„Bloczek zwracany przez innego strażnika”,
„Odcinek o tym numerze już wprowadzono”,
„Nie wydano bloczku mogącego zawierać taki numer”,
„Data ukarania wcześniejsza niż data wydania bloczku”,
„Data ukarania większa niż dzisiaj”,
„Takiego odcinka nie wprowadzono”
}
*******************EWIDENCJA*******************
| id_strażnika: NUMER_STRAŻNIKA (imię x nazwisko)
| id_bloczku: NUMER_BLOCZKU (ilość_odcinków_w_bloczku x numer_strażnika x data_pobrania x
| data_zwrotu x ilość_odcinków_niewykorzystanych x oddany)
| id_odcinek_b: NUMER_ODCINKA (numer_strażnika x data_ukarania x kwota_mandatu x
| nazwisko_ukaranego x imie_ukaranego x pesel x
| symbol_dokumentu_tozsamosci x numer_dokumentu_tozsamosci x adres)
| id_odcinek_d: NUMER_ODCNIKA (kwota_mandatu x data_zaplaty)
STRAŻNICY
| strażnik: P.(numer_straznika x imie x nazwisko)
| 0 ≤ numer_strażnika
BLOCZKI
| bloczek: P (numer_bloczku x ilość_odcinków_w_bloczku x numer_strażnika x data_pobrania x
| data_zwrotu x ilość_odcinków_niewykorzystanych x oddany)
| 0 ≤ numer_bloczku
ODCINKI_B
| odcinek_b: P (numer_odcinka x numer_strażnika x data_ukarania x kwota_mandatu x nazwisko_ukaranego
| x imie_ukaranego x pesel x symbol_dokumentu_tozsamosci x numer_dokumentu_tozsamosci
x adres)
| 0 ≤ numer_odcinka
| 0 ≤ kwota_mandatu ≥ 500
ODCINKI_D
| odcinek_d: P (numer_odcinka x kwota_mandatu x data_zaplaty)
| 0 ≤ numer_odcinka
| 0 ≤ kwota_mandatu ≥ 500
Init_Strażnicy
| Strażnicy
| strażnicy = ∅
Init_Bloczki
| Bloczki
| bloczki = ∅
Init_ODCINKI_B
| Odcinki_b
| odcinki_b = ∅
Init_ODCINKI_D
| Odcinki_d
| odcinki_b = ∅
Dodaj strażnika
| Δ strażnicy
| numer_strażnika?: NUMER_STRAŻNIKA
| imie?: IMIE
| nazwisko?:NAZWISKO
| kom?: KOMUNIKAT
| (numer_strażnika? ∉ dom strażnicy
| strażnicy'=strażnicy ∪ {numer?, imie?, nazwisko?}) ∨
| (numer_strażnika? ∈ dom strażnicy
| kom! = „Straznik o takim numerze juz istnieje”)
Edycja strażnika
| Δ strażnicy
| numer_strażnika?: NUMER_STRAŻNIKA
| imie?: IMIE
| nazwisko?:NAZWISKO
| kom?: KOMUNIKAT
| (numer_strażnika? ∈ dom strażnicy
| strażnicy'=strażnicy ⊕ {id_strażnika(numer_straznika?).imie = imie?,
| id_strażnika(numer_straznika?).nazwisko = nazwisko?}) ∨
| (numer_strażnika? ∉ dom strażnicy
| kom! = „Nie ma takiego strażnika”)
Usuń strażnika
| Δ strażnicy
| numer_strażnika?: NUMER_STRAŻNIKA
| kom?: KOMUNIKAT
| (numer_strażnika? ∈ dom strażnicy
| strażnicy'= strażnicy \ {numer_strażnika?, imie?, nazwisko?}) ∨
| (numer_strażnika? ∉ dom strażnicy
| kom! = „Nie ma takiego strażnika”)
Dodaj bloczek
| Δ bloczki
| numer_bloczku?: NUMER_BLOCZKU
| numer_strażnika?: NUMER_STRAŻNIKA
| ilość_odcinków_w_bloczku?: ILOŚĆ_ODCINKÓW_W_BLOCZKU
| data_pobrania?: DATA
| kom?: KOMUNIKAT
| (numer_bloczku? ∉ dom bloczki
| bloczki'= bloczki ∪ {numer_bloczku?, numer_straznika?, ilość_odcinków_w_bloczku?,
| data_pobrania?}, ∧
| bloczki' = bloczki ⊕ {id_bloczku(numer_bloczku?).oddany = „nie” ) ∨
| (numer_bloczku? ∈ dom bloczki
| kom! = „Taki bloczek już wydano”) ∨
| (numer_bloczku? ∉ dom bloczki ∧ data_pobrania? > dziś
| kom! = „Data pobrania późniejsza niż dzisiaj”)
Oddaj bloczek
| Δ bloczki
| numer_bloczku?: NUMER_BLOCZKU
| numer_strażnika?: NUMER_STRAŻNIKA
| data_zwrotu?: DATA
| ilość_odcinków_niewykorzystanych?: ILOŚĆ_ODCINKÓW_NIEWYKORZYSTANYCH
| kom?: KOMUNIKAT
| (numer_bloczku? ∈ dom bloczki
| bloczki'= bloczki ⊕ {id_bloczku(numer_bloczku?).data_zwrotu?,
| id_bloczku(numer_bloczku?).ilość_odcinków_niewykorzystanych?,
| id_bloczku(numer_bloczku?).oddany = „tak” }) ∨
| (numer_bloczku? ∉ dom bloczki
| kom! = „Nie wydano takiego bloczku”) ∨
| (numer_bloczku? ∈ dom bloczki ∧ id_bloczku(numer_bloczku?).oddany = „tak
| kom! = „Ten bloczek już zwrócono”) ∨
| (numer_bloczku? ∈ dom bloczki ∧
| id_bloczku(numer_bloczku?).data_wydania > data_zwrotu?
| kom! = „Data zwrotu wcześniejsza od daty wydania”) ∨
| (numer_bloczku? ∈ dom bloczki ∧ numer_straznika ∉ dom straznicy
| kom! = „Bloczek zwracany przez nieistniejącego straznika”) ∨
| (numer_bloczku? ∈ dom bloczki ∧ id_bloczku(numer_bloczku?).numer_strażnika <> numer_strażnika?
| kom! = „Bloczek zwracany przez innego strażnika”)
Dodaj odcinek_b
| Δ odcinki_b
| numer_odcinka?: NUMER_ODCINKA
| numer_bloczku? : NUMER_BLOCZKU
| numer_strażnika?: NUMER_STRAŻNIKA
| data_ukarania?: DATA
| kwota_mandatu?: KWOTA_MANDATU
| nazwisko_ukaranego?: NAZWISKO
| imie_ukaranego?: IMIE
| pesel?: PESEL
| symbol_dokumentu_tozsamości?: SYMBOL_DOKUMENTU_TOŻSAMOŚCI
| numer_dokumentu_tożsamości?: NUMER_DOKUMENTU_TOZSAMOSCI
| adres?: ADRES
| kom?: KOMUNIKAT
| (numer_odcinka? ∉ dom odcinki_b
| odcinki_b'= odcinki_b ∪ {numer_odcinka?, numer_bloczku?, numer_straznika?, data_ukarania?,
| kwota_mandatu?, nazwisko_ukaranego?, imie_ukaranego?, pesel?, symbol_dokumentu_tożsamości?,
| numer_dokumentu_tożsamości?, adres? }) ∨
| (numer_odcinka? ∈ dom odcinki_b
| kom! = „Odcinek o tym numerze już wprowadzono”) ∨
| (numer_odcinka? ∉ dom odcinki_b ∧ numer_odcinka ∉ { numer_bloczku? ..
| numer_bloczku + id_bloczku(numer_bloczku?).ilość_odcinków_niewykorzystanych }
| kom! = „Nie wydano bloczku mogącego zawierać taki numer”) ∨
| (numer_odcinka_? ∉ dom odcinki_b ∧ data_ukarania? < id_bloczku(numer_bloczku?).data_pobrania
| kom! = „Data ukarania wcześniejsza niż data wydania bloczku”) ∨
| (numer_odcinka? ∉ dom odcinki_b ∧ data_ukarania? > dziś
| kom! = „Data ukarania większa niż dzisiaj”) ∨
Usuń odcinek_b
| Δ odcinki_b
| numer_odcinka?: NUMER_ODCINKA
| numer_odcinka? ∈ dom odcinki_b
| odcinki_b'= odcinki_b \ {id_odcinki_b(numer_odcinka?).*
| (numer_odcinka? ∉ dom odcinki_b
| kom! = „Takiego odcinka nie wprowadzono”) ∨
Edytuj odcinek_b
| Δ odcinki_b
| numer_odcinka?: NUMER_ODCINKA
| numer_bloczku? : NUMER_BLOCZKU
| numer_strażnika?: NUMER_STRAŻNIKA
| data_ukarania?: DATA
| kwota_mandatu?: KWOTA_MANDATU
| nazwisko_ukaranego?: NAZWISKO
| imie_ukaranego?: IMIE
| pesel?: PESEL
| symbol_dokumentu_tozsamości?: SYMBOL_DOKUMENTU_TOŻSAMOŚCI
| numer_dokumentu_tożsamości?: NUMER_DOKUMENTU_TOZSAMOSCI
| adres?: ADRES
| kom?: KOMUNIKAT
| (numer_odcinka? ∈ dom odcinki_b
| odcinki_b'= odcinki_b ⊕ {id_odcinki_b(numer_odcinka?).numer_strażnika = numer_straznika?,
| id_odcinki_b(numer_odcinka?).data_ukarania = data_ukarania?,
| id_odcinki_b(numer_odcinka?).kwota_mandatu = kwota_mandatu?,
| id_odcinki_b(numer_odcinka?).nazwisko_ukaranego = nazwisko_ukaranego?,
| id_odcinki_b(numer_odcinka?).imie_ukaranego = imie_ukaranego?,
| id_odcinki_b(numer_odcinka?).pesel = pesel?,
| id_odcinki_b(numer_odcinka?).symbol_dokumentu_tożsamości = symbol_dokumentu_tożsamości?,
| id_odcinki_b(numer_odcinka?).numer_dokumentu_tożsamości = numer_dokumentu_tożsamości?,
| id_odcinki_b(numer_odcinka?).adres = adres? }) ∨
| (numer_odcinka? ∉ dom odcinki_b
| kom! = „Nie ma takiego odcinka”) ∨
| (numer_odcinka? ∉ dom odcinki_b ∧ numer_odcinka ∉ { numer_bloczku? ..
| numer_bloczku? + id_bloczku(numer_bloczku?).ilość_odcinków_niewykorzystanych }
| kom! = „Nie wydano bloczku mogącego zawierać taki numer”) ∨
| (numer_odcinka_? ∉ dom odcinki_b ∧ data_ukarania? < id_bloczku(numer_bloczku?).data_pobrania
| kom! = „Data ukarania wcześniejsza niż data wydania bloczku”) ∨
| (numer_odcinka? ∉ dom odcinki_b ∧ data_ukarania? > dziś
| kom! = „Data ukarania większa niż dzisiaj”) ∨
Dodaj odcinek_d
| Δ odcinki_d
| numer_bloczku : NUMER_BLOCZKU
| numer_odcinka?: NUMER_ODCINKA
| kwota_mandatu?: KWOTA_MANDATU
| data_zapłaty: DATA
| kom?: KOMUNIKAT
| (numer_odcinka? ∉ dom odcinki_d
| odcinki_d'= odcinki_d ∪ {numer_odcinka?, kwota_mandatu?, data_zapłaty}) ∨
| (numer_odcinka? ∈ dom odcinki_d
| kom! = „Odcinek o tym numerze już wprowadzono”) ∨
| (numer_odcinka? ∉ dom odcinki_d ∧ numer_odcinka ∉ { numer_bloczku? ..
| numer_bloczku + id_bloczku(numer_bloczku?).ilość_odcinków_niewykorzystanych }
| kom! = „Nie wydano bloczku mogącego zawierać taki numer”) ∨
| (numer_odcinka_? ∉ dom odcinki_d ∧ data_zapłaty? < id_odcinki_b(numer_odcinka?).data_pobrania
| kom! = „Data zapłaty wcześniejsza niż data wydania bloczku”) ∨
| (numer_odcinka? ∉ dom odcinki_d ∧ data_zapłaty? > dziś
| kom! = „Data zapłaty większa niż dzisiaj”) ∨
Usuń odcinek_d
| Δ odcinki_d
| numer_odcinka?: NUMER_ODCINKA
| numer_odcinka? ∈ dom odcinki_d
| odcinki_d'= odcinki_d \ {id_odcinki_d(numer_odcinka?).*
| (numer_odcinka? ∉ dom odcinki_d
| kom! = „Takiego odcinka nie wprowadzono”) ∨
Edytuj odcinek_b
| Δ odcinki_d
| numer_odcinka?: NUMER_ODCINKA
| numer_bloczku? : NUMER_BLOCZKU
| kwota_mandatu?: KWOTA_MANDATU
| data_zapłaty?: DATA
| kom?: KOMUNIKAT
| (numer_odcinka? ∈ dom odcinki_d
| odcinki_d'= odcinki_d ⊕ { id_odcinki_d(numer_odcinka?).numer_bloczku = numer_bloczku?,
| id_odcinki_d(numer_odcinka?).kwota_mandatu = kwota_mandatu?,
| id_odcinki_d(numer_odcinka?).data_zapłaty = data_zapłaty?,
| (numer_odcinka? ∉ dom odcinki_d
| kom! = „Nie ma takiego odcinka”) ∨
| (numer_odcinka_? ∉ dom odcinki_d ∧ data_ukarania? < id_bloczku(numer_bloczku?).data_pobrania
| kom! = „Data zapłaty wcześniejsza niż data wydania bloczku”) ∨
| (numer_odcinka? ∉ dom odcinki_d ∧ data_ukarania? > dziś
| kom! = „Data zapłaty większa niż dzisiaj”) ∨