Μοντελοποίηση των κανόνων του παιχνιδιού Blackjack με τυπικές μεθόδους

Στίγγας, Κρίτωνας

Modeling rules of Blackjack using formal methods

Διπλωματική εργασία

Author

Στίγγας, Κρίτωνας

Date

2024-03-21

Advisor

Barlas, Konstantinos

iceuniwa_171119.pdf (949.0Kb)

Keywords

Τυπικές μέθοδοι ; Αλγεβρικές γλώσσες προδιαγραφών ; CafeOBJ ; Απόδειξη θεωρήματος ; Μέθοδος Coinduction

Abstract

Αντικείμενο τις διπλωματικής εργασίας αποτελεί η εφαρμογή των Tυπικών Mεθόδων για τη μοντελοποίηση και επαλήθευση των κανόνων παιχνιδιού BlackJack χρησιμοποιώντας αλγεβρικές προδιαγραφές. Οι αλγεβρικές προδιαγραφές οι οποίες είναι γλώσσες, τεχνικές και εργαλεία βασισμένες στα μαθηματικά, παρέχουν τη δυνατότητα να αναλύσουμε και να επαληθεύσουμε τις ιδιότητες του συστήματος, περιγράφοντας το μέσω μιας αυστηρά μαθηματικά ορισμένης προδιαγραφής. Μέσω τις εκτελέσιμης γλώσσας αλγεβρικών προδιαγραφών CafeOBJ και με την ενσωμάτωση συμπεριφοριακών προδιαγραφών, το παραγόμενο μοντέλο περιγράφει σε μορφή αλγεβρικής οντότητας το παιχνίδι και επιτρέπει τη μελέτη της οντότητας σε κάθε πιθανή κατάσταση θωρακίζοντας το από κακό σχεδιασμό κανόνων.

Abstract

The subject of the thesis is the application of formal methods for modeling and verifying BlackJack game rules using algebraic specifications. Algebraic specifications which are languages, techniques and tools based on mathematics, provide the possibility to analyze and verify the properties of the system by describing it through a rigorously mathematically defined specification. Through the executable algebraic specification language CafeOBJ and the integration of behavioral specifications, the generated model describes the game in the form of an algebraic entity and allows the entity to be studied in every possible situation, protecting it from bad rule design.