Ζωνιανά

Πραγματικά θλίψη μου προκαλεί η εικόνα της Κρήτης και ιδιαίτερα της επ. Μυλοποτάμου από την οποία κατάγομαι, τα τελευταία χρόνια. Από "Ρέθυμνο των γραμμάτων και των τεχνών" έχουμε καταντήσει Ρέθυμνο της αρπακτής, των ναρκωτικών και της εγκληματικότητας. Είναι φυσικό ότι όλα αυτά που βγαίνουν τώρα στην δημοσιότητα ήταν λίγο πολύ γνωστά, ειδικά για τους κατοίκους του νησιού. Δεν είναι δυνατό να βλέπεις άτομα αγράμματα, που δήλωνουν ως επάγγελμα βοσκοί να κυκλοφορούν με πανάκριβα αυτοκίνητα, να αγοράζουν τα καλύτερα μαγαζιά σε Πέραμα και Ρέθυμνο, να έχουν στην κατοχή τους πολυτελή ξενοδοχεία χωρίς να ισχύει για αυτούς νόμος. Στο κέντρο του χωριού μου, στο Πέραμα, ουκ ολίγες φορές εκτυλίχθηκαν σκηνές φαρ ουεστ, λίγα μέτρα από το αστυνομικό τμήμα, χωρις την επέμβαση της αστυνομίας. Όταν κάποιοι προσπάθησαν να διαμαρτυρηθούν για την όλη κατάσταση ή να κάνουν κάτι, βρήκαν το μπελά τους. Γνωστοί στην περιοχή καλλιεργητές και εμπόροι χασις πλουτίζουν, ενώ όσοι φυλακίσθηκαν, βγήκαν νωρίτερα από τους απλούς χρήστες, οι οποίοι στο κάτω κάτω τον εαύτο τους βλάπτουν.
Σίγουρα, οι αιτίες του προβλήματος είναι πολυδιάστατες: Μεγάλο μερίδιο ευθύνης φέρει η πολιτεία η οποία κατά καιρούς, και όταν πλέον δεν πάει άλλο, κάνει κινήσεις εντυπωσιασμού για να πει ότι κάτι έγινε. Φταίει η αστυνομία, γιατί δεν έχει ξεκαθαρίσει ακόμα από τους επίορκους αστυνομικούς, και γιατί για να κάνει κάτι πρέπει να χτυπηθεί μέλος της. Το σύνθημα των αναρχικών "Ποιός θα μας φυλάξει από τους Φύλακες", είναι πιο επίκαιρο από ποτέ.
Τέλος, δεν επιτρέπεται να μας κοροιδεύουν από τις τηλεοράσεις ορισμένοι πολιτικοί οι οποίοι κάνουν τώρα τους τιμητές, ενώ είναι γνωστό το ποιόν τους, τραγουδιστές παρακμιακών κρητικών ασμάτων "Ηρθαν οι ειδικοί φρουροί και έχω μεγάλη ευθύνη, γιατί τα όπλα του χωριού επήρα υπευθύνη", εξηγώντας ότι όταν φωνάζουν "Στ' άρματα" στα γλέντια, καλούν τους πολίτες να εξεγερθούν ενάντια στο κατεστημένο, και απλοί πολίτες οι οποίοι λένε ότι οι χασισοκαλλιεργητές-εγκληματίες-ζωοκλέφτες- είναι μια μικρή μειοψηφία της κοινωνίας. Δυστυχώς, σε χωριά όπως τα Ζωνιανά, είναι η μεγάλη πλειοψηφία. Γιατί όσους σοβαρούς ανθρώπους έχω γνωρίσει από τα εν λόγω χωριά έχουν αυτο-εξοριστεί μην αντέχοντας την κατάντια της περιοχής τους και των ανθρώπων της. Ας ελπίσουμε ότι, έστω και με αφορμή τον σοβαρό τραυματισμό του ειδικού φρουρού, γίνει κάτι δραστικό και μόνιμο.

Prof. Futatsugi's talk

It is our pleasure that Prof. Kokichi Futatsugi will talk about current trends in the verification of formal specifications with proof scores in CafeOBJ Algebraic Specification Language. The talk shall take place next Friday, November 9th, 12:00, at the Department of Mathematics of National Technical University of Athens.


=================================================
Title, Abstract, and Short Bio
=================================================

Title:

Verifying Specifications with Proof Scores in CafeOBJ
by Kokichi FUTATSUGI
Graduate School of Information Science
JAIST (Japan Advanced Institute of Science and Technology)
Nomi, Ishikawa, Japan

Abstract:

Verifying specifications is still one of the most important
undeveloped topics in software engineering. It is important because
quite a few critical bugs are caused at the level of domains,
requirements, and/or designs. It is also important for the cases where
no program codes are generated and specifications are analyzed/
verified only for justifying models of problems in real world. In
this talk, a survey of our research activities in verifying
specifications is given. After explaining fundamental issues and
importance of verifying specifications, the proof score approach in
CafeOBJ and its applications to several areas are described.


Short Bio of KF:

Kokichi Futatsugi is a professor of Graduate School of Information
Science, JAIST (Japan Advanced Institute of Science and Technology),
Ishikawa, Japan. His research interest includes formal methods,
software requirements and specifications, modeling and specification
languages. An important part of his research activities is done
around the CafeOBJ formal specification language
(www.ldl.jaist.ac.jp/cafeobj). CafeOBJ is an executable formal
specification language which has been designed and developed by an
international team headed by Prof. Futatsugi. He was a co-chair of
the program committee of the 20th International Conference on Software
Engineering (ICSE 1998) and an associate editor of ACM TOSEM
(Transaction of Software Engineering and Methodology) for 1995-2002.
He is a member of the advisory board of Journal of Higher-Order and
Symbolic Computation (www.wkap.nl/journals/hosc), and the editorial
board of Journal of Object Technology (www.jot.fm) and Journal of
Applied Logic (www.elsevier.com/locate/jal).
=================================================