Στατική ανάλυση

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

Στην πληροφορική, στατική ανάλυση, στατική ανάλυση κώδικα ή στατική ανάλυση προγράμματος (Αγγλ.: static analysis, static code analysis, static program analysis), είναι η ανάλυση ενός προγράμματος που γίνεται χωρίς να εκτελεστεί το πρόγραμμα (η ανάλυση προγράμματος που γίνεται με εκτέλεσή του λέγεται δυναμική ανάλυση). Στις περισσότερες περιπτώσεις η ανάλυση γίνεται σε κάποιο επίπεδο πηγαίου κώδικα και πολλές φορές σε αντικειμενικό κώδικα. Ο όρος συνήθως αναφέρεται στην ανάλυση που γίνεται με κάποιο αυτόματο εργαλείο, ενώ η ανάλυση προγράμματος από άνθρωπο λέγεται κατανόηση προγράμματος.

Η ανάλυση που μπορεί να γίνει από αυτόματα εργαλεία ποικίλλει από αυτά που εξετάζουν τη συμπεριφορά μόνο συγκεκριμένων εκφράσεων ή δηλώσεων στο πρόγραμμα, έως αυτά που συμπεριλαμβάνουν ολόκληρο τον πηγαίο κώδικα ενός προγράμματος στην ανάλυση. Οι χρήσεις των πληροφοριών που πηγάζουν από την ανάλυση συμπεριλαμβάνουν από τον εντοπισμό πιθανών λαθών στο πρόγραμμα (π.χ. το εργαλείο lint), έως τυπικές μεθόδους που αποδεικνύουν μαθηματικά ιδιότητες για κάποιο δεδομένο πρόγραμμα (π.χ. ότι η συμπεριφορά του όντως ακολουθεί την τεχνική του περιγραφή).

Η μέτρηση μιας οποιασδήποτε ιδιότητας του προγράμματος, όπως και ο αντίστροφος σχεδιασμός (reverse engineering) θεωρούνται επίσης είδη στατικής ανάλυσης.

Μια αυξανόμενη εμπορική χρήση της στατικής ανάλυσης είναι η επαλήθευση ιδιοτήτων του λογισμικού που χρησιμοποιείται σε υπολογιστικά συστήματα όπου η ασφάλεια είναι κρίσιμη, για την αυτόματη ανακάλυψη πιθανών τρωτών σημείων στον κώδικα.

Τυπικές μέθοδοι[Επεξεργασία | επεξεργασία κώδικα]

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

Αν υποθέσουμε ότι ο χώρος καταστάσεων των προγραμμάτων δεν είναι πεπερασμένος και μικρός, τότε αποδεικνύεται πως η εύρεση όλων των δυνατών λαθών χρόνου εκτέλεσης ή γενικότερα οποιουδήποτε είδους παραβίαση των προδιαγραφών στο τελικό αποτέλεσμα ενός προγράμματος, είναι αδύνατη: δεν υπάρχει καμία αυτόματη μηχανική μέθοδος που να μπορεί πάντα να βρίσκει με ακρίβεια αν ένα πρόγραμμα έχει λάθη εκτέλεσης ή όχι. Το αποτέλεσμα αυτό προκύπτει από τις εργασίες των Αλόνζο Τσερτς, Κουρτ Γκέντελ και Άλαν Τούρινγκ στη δεκαετία του 1930 (βλ. πρόβλημα τερματισμού και θεώρημα Ράις). Όπως συμβαίνει με τα περισσότερα άλυτα προβλήματα απόφασης, μπορεί κανείς να προσπαθήσει να δώσει χρήσιμες προσεγγιστικές λύσεις.

Κάποιες από τις τεχνικές υλοποίησης της τυπικής στατικής ανάλυσης είναι:

  • Ο έλεγχος μοντέλων (model checking) εξετάζει συστήματα που έχουν πεπερασμένη κατάσταση, ή μπορούν να αναχθούν σε πεπερασμένη κατάσταση με αφαίρεση
  • Η ανάλυση ροής δεδομένων (data-flow analysis) βασίζεται σε δομές συνδέσμων (lattices) για τη συλλογή πληροφοριών για το πιθανό σύνολο τιμών
  • Η αφηρημένη διερμηνεία (abstract interpretation) μοντελοποιεί το αποτέλεσμα κάθε εντολής στην κατάσταση μιας αφηρημένης μηχανής (δηλαδή 'εκτελεί' το πρόγραμμα βασιζόμενη στις μαθηματικές ιδιότητες κάθε εντολής). Η αφηρημένη αυτή μηχανή προσεγγίζει όλες τις δυνατές συμπεριφορές του συστήματος. Έτσι, το αφηρημένο σύστημα είναι ευκολότερο να αναλυθεί μαθηματικά, με κόστος την μη πληρότητα της ανάλυσης (δεν ισχύει πάντα κάθε ιδιότητα του πραγματικού και για το αφηρημένο). Αν γίνει σωστά, παρ' όλα αυτά, η αφηρημένη διερμηνεία είναι συνεπής (κάθε ιδιότητα του αφηρημένου ισχύει και για το πραγματικό).
  • Η χρήση ισχυρισμών στον κώδικα ενός προγράμματος όπως προτάθηκε αρχικά στη λογική Χόαρ. Υπάρχουν εργαλεία που την υποστηρίζουν για κάποιες γλώσσες προγραμματισμού, όπως η SPARK, ένα υποσύνολο της Ada και η JML (με χρήση του ESC/Java και του ESC/Java2).

Σχετικά άρθρα[Επεξεργασία | επεξεργασία κώδικα]

Εξωτερικοί σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Βιβλιογραφία[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Static code analysis της Αγγλικής Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).