Ιδιότητα προς επαλήθευση
- Στόχος: μία συνάρτηση πολιτικής επιστροφών
- Είσοδοι: μη αρνητικοί ακέραιοι
- Εξωτερικό I/O, βάση δεδομένων και δίκτυο είναι εκτός πεδίου
- Ελέγχεται μέσα σε ρητές παραδοχές και υποσύνολο της Go
MPK Assurance / Έλεγχος ετοιμότητας απόδειξης για Go
Ελέγχουμε μηχανικά κρίσιμη λογική Go που χειρίζεται χρήματα, όπως επιστροφές, χρεώσεις, υπόλοιπα και αποθεματικά, με βάση ρητές προδιαγραφές, παραδοχές και πεδίο. Το Gemini προετοιμάζει υποψήφιες αποδείξεις και ο ανεξάρτητος πυρήνας MPK δίνει την τελική κρίση.
Για τις πρώτες 5 εταιρείες Προσφορά πρώτης εφαρμογής MPK JPY 49,800(προ φόρου)func ApplyRefund(paid, refunded, amount int64) (int64, error) {
if amount < 0 {
return refunded, errors.New("negative amount")
}
if refunded+amount > paid {
return refunded, errors.New("exceeds paid")
}
return refunded + amount, nil
}
∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
paid=100, refunded=80, amount=30 παραβιάζει την ιδιότητα.
Ο πυρήνας αποδέχτηκε το διορθωμένο κανονικό πιστοποιητικό.
Επίδειξη επιστροφής 30 δευτερολέπτων
Δοκιμάστε τον έτοιμο κώδικα επιστροφής και δείτε τη ροή από το αντιπαράδειγμα στη διόρθωση και στην επιτυχημένη απόδειξη. Δεν χρειάζεται να εισαγάγετε εμπιστευτικό κώδικα στη δημόσια επίδειξη.
Πολιτική επιστροφών: οι συνολικές επιστροφές δεν πρέπει να υπερβαίνουν το πληρωμένο ποσό
Βρήκαμε συγκεκριμένες εισόδους όπου η συνολική επιστροφή υπερβαίνει το πληρωμένο ποσό.
Κατηγοριοποίηση αποτελεσμάτων
Η καθορισμένη ιδιότητα ισχύει υπό τις ρητές παραδοχές και το πεδίο.
ΑΠΟΔΕΔΕΙΓΜΕΝΟΔείχνουμε συγκεκριμένες εισόδους που παραβιάζουν την ιδιότητα και ξεκαθαρίζουμε ποια συνθήκη χρειάζεται διόρθωση.
ΔΙΑΨΕΥΣΤΗΚΕΑναφέρουμε ξεκάθαρα όταν η τρέχουσα στρατηγική δεν μπορεί να κρίνει αν η ιδιότητα ισχύει.
ΑΓΝΩΣΤΟΕξηγούμε τους συγκεκριμένους λόγους για τους οποίους δεν μπορούμε να καλύψουμε τον στόχο, όπως μη υποστηριζόμενη σύνταξη, εξωτερικό I/O ή μη υποστηριζόμενη συμπεριφορά.
ΜΗ ΕΦΑΡΜΟΣΙΜΟΔιαφορά από τις δοκιμές
| Σύγκριση | Δοκιμές | Απόδειξη |
|---|---|---|
| Στόχος | Επιλεγμένες είσοδοι | Καθορισμένη ιδιότητα |
| Εμφάνιση αντιπαραδείγματος | △ | ○ |
| Επανέλεγχος | Αρχείο εκτέλεσης | Πιστοποιητικό |
| Τελική κρίση | Σύνολο δοκιμών | Πυρήνας |
Ελέγχουμε την ιδιότητα με βάση ρητές προδιαγραφές, παραδοχές και πεδίο, όχι μόνο με λίγες ενδεικτικές εισόδους.
Μπορείτε να ξεκινήσετε με μια κρίσιμη συνάρτηση πολιτικής σε Go, απομονωμένη από εξωτερικό I/O.
Η τεχνητή νοημοσύνη μόνο προετοιμάζει υποψήφια στοιχεία. Η τελική αποδοχή γίνεται από ανεξάρτητο πυρήνα που διαβάζει το κανονικό πιστοποιητικό.
Το Gemini εκτελεί τη ροή απόδειξης, το MPK παίρνει την απόφαση εμπιστοσύνης και άνθρωπος εγκρίνει την παράδοση.
Πακέτο τεκμηρίωσης
Έλεγχος ετοιμότητας απόδειξης
Κανονική εγγραφή πιστοποιητικού
Έλεγχος ετοιμότητας απόδειξης
Αυτή είναι η προγραμματισμένη τυπική τιμή. Αυτή την περίοδο τρέχει καμπάνια πρώτης εφαρμογής για τις πρώτες 5 εταιρείες, με JPY 49,800 προ φόρου.
Προσφορά πρώτης εφαρμογής MPK
Για τις πρώτες 5 εταιρείεςΣτον έλεγχο ετοιμότητας απόδειξης MPK επιλέγουμε μία στοχευμένη συνάρτηση Go, ορίζουμε την ιδιότητα που πρέπει να εγγυηθεί, δημιουργούμε υποψήφιες αποδείξεις με τεχνητή νοημοσύνη και εκτελούμε ανεξάρτητο έλεγχο με τον πυρήνα MPK.
Η προσφορά αφορά εταιρείες που μπορούν να δώσουν ειλικρινή σχόλια μετά την υπηρεσία και να εγκρίνουν μελέτη περίπτωσης για δημοσίευση στον επίσημο ιστότοπο MPK. Η μελέτη μπορεί να περιλαμβάνει επωνυμία εταιρείας, όνομα υπεύθυνου, τίτλο, σχόλια και είτε αντιπροσωπευτική φωτογραφία είτε λογότυπο εταιρείας.
Ροή υπηρεσίας
Επιβεβαιώνουμε το σενάριο αστοχίας που θα μπορούσε να προκαλέσει απώλεια και τη στοχευμένη συνάρτηση.
Κλειδώνουμε τη συνάρτηση, την ιδιότητα, τις παραδοχές και το εξαιρούμενο πεδίο.
Η τεχνητή νοημοσύνη προετοιμάζει υποψήφια στοιχεία και το MPK ελέγχει το πιστοποιητικό.
Εξηγούμε την απόδειξη, το αντιπαράδειγμα, το άγνωστο αποτέλεσμα, τις εξαιρέσεις και τα αποδεικτικά στοιχεία.
Ξεκαθαρίζουμε αν πρέπει να προχωρήσουμε σε διορθώσεις, πρόσθετες συναρτήσεις ή ενσωμάτωση CI/CD.
Συχνές ερωτήσεις
Οι απαντήσεις καλύπτουν συχνές ερωτήσεις πριν επικοινωνήσετε μαζί μας, όπως το πεδίο απόδειξης, τον ρόλο της τεχνητής νοημοσύνης και τον χειρισμό του κώδικα.
Όχι. Ελέγχουμε μόνο την καθορισμένη ιδιότητα μέσα στις ρητές παραδοχές, το πεδίο και το υποστηριζόμενο υποσύνολο της Go. Αυτό δεν εγγυάται ολόκληρη την εφαρμογή ή εξωτερικά συστήματα.
Όχι για τον πρώτο έλεγχο. Ξεκινάμε επιβεβαιώνοντας μια συνάρτηση πολιτικής σε Go, απομονωμένη από εξωτερικό I/O, και την ιδιότητα που θέλετε να εγγυηθείτε.
Όχι. Το Gemini δημιουργεί ιδιότητες, στρατηγικές απόδειξης και υποψήφιες αποδείξεις. Ο ανεξάρτητος πυρήνας MPK αποδέχεται ή απορρίπτει το τελικό πιστοποιητικό.
Κατατάσσουμε το αποτέλεσμα ως αντιπαράδειγμα, άγνωστο ή εκτός πεδίου και μετά εξηγούμε τον λόγο, τις απαιτούμενες προδιαγραφές, τις πιθανές διορθώσεις και πώς να απομονωθεί μια αποδείξιμη μονάδα.
Αφού ο έλεγχος ετοιμότητας απόδειξης επιβεβαιώσει τον στόχο και την εφικτότητα της απόδειξης, μπορούμε να προτείνουμε ξεχωριστά συνεχείς ελέγχους ή ενσωμάτωση CI/CD.
Δεν χρειάζεται να επικολλήσετε εμπιστευτικό κώδικα στη δημόσια φόρμα. Μετά το ερώτημα, θα επιβεβαιώσουμε τον χειρισμό NDA και ασφαλή τρόπο κοινοποίησης.
Επικοινωνία
Πείτε μας ποια αστοχία θα είχε τη μεγαλύτερη σημασία και ποια συνάρτηση Go θέλετε να ελεγχθεί. Δεν χρειάζεται να επικολλήσετε εμπιστευτικό κώδικα στη δημόσια φόρμα.
Υποστηρίζονται NDA και ασφαλής κοινοποίηση κώδικα