MPK Assurance / przegląd gotowości do dowodu dla Go
Mechanicznie sprawdzamy krytyczną logikę Go, która zmienia stan środków, taką jak zwroty, opłaty, salda i rezerwy, względem jawnych specyfikacji, założeń i zakresu. Gemini przygotowuje kandydatów dowodu, a niezależne jądro MPK wydaje ostateczny werdykt.
Tylko dla pierwszych 5 firm Oferta wczesnego wdrożenia MPK JPY 49,800(przed opodatkowaniem)
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 narusza własność.
Jądro zaakceptowało poprawiony certyfikat kanoniczny.
30-sekundowe demo zwrotu
Wypróbuj przygotowany kod zwrotu i zobacz przejście od kontrprzykładu przez poprawkę do udanego dowodu. W publicznym demo nie trzeba wpisywać poufnego kodu.
Polityka zwrotów: łączne zwroty nie mogą przekroczyć zapłaconej kwoty
Znaleźliśmy konkretne dane wejściowe, przy których łączny zwrot przekracza zapłaconą kwotę.
Klasyfikacja wyników
Wskazana własność obowiązuje przy jawnych założeniach i zakresie.
UDOWODNIONEPokazujemy konkretne dane wejściowe naruszające własność i wyjaśniamy, który warunek trzeba poprawić.
SFALSYFIKOWANEJasno raportujemy, gdy obecna strategia nie potrafi ustalić, czy własność obowiązuje.
NIEUSTALONEWyjaśniamy konkretne powody, dla których nie możemy obsłużyć celu, takie jak nieobsługiwana składnia, zewnętrzne I/O lub nieobsługiwane zachowanie.
NIE DOTYCZYRóżnica względem testowania
| Porównanie | Testowanie | Dowód |
|---|---|---|
| Cel | Wybrane dane wejściowe | Wskazana własność |
| Pokazanie kontrprzykładu | △ | ○ |
| Ponowne sprawdzenie | Dziennik wykonania | Certyfikat |
| Ostateczna ocena | Zestaw testów | Jądro |
Sprawdzamy własność względem jawnych specyfikacji, założeń i zakresu, a nie tylko kilku przykładowych danych wejściowych.
Możesz zacząć od krytycznej funkcji reguł w Go, odizolowanej od zewnętrznego I/O.
SI tylko przygotowuje kandydatów. Ostateczną akceptację wykonuje niezależne jądro, które odczytuje certyfikat kanoniczny.
Gemini uruchamia przepływ dowodowy, MPK podejmuje decyzję zaufania, a człowiek zatwierdza dostarczenie wyniku.
Pakiet dowodowy
Przegląd gotowości do dowodu
Kanoniczny zapis certyfikatu
Przegląd gotowości do dowodu
To planowana cena standardowa. Obecnie prowadzimy kampanię wczesnego wdrożenia ograniczoną do pierwszych 5 firm, w cenie JPY 49,800 przed opodatkowaniem.
Oferta wczesnego wdrożenia MPK
Tylko dla pierwszych 5 firmW przeglądzie gotowości do dowodu MPK wybieramy jedną docelową funkcję Go, definiujemy własność do zagwarantowania, generujemy kandydatów dowodu z pomocą SI i uruchamiamy niezależne sprawdzenie w jądrze MPK.
Oferta jest przeznaczona dla firm, które po zakończeniu usługi mogą przekazać szczerą opinię i zatwierdzić opis przypadku do publikacji na oficjalnej stronie MPK. Opis przypadku może obejmować nazwę firmy, imię i nazwisko osoby kontaktowej, stanowisko, opinię oraz zdjęcie reprezentacyjne albo logo firmy.
Przebieg usługi
Potwierdzamy scenariusz awarii, który mógłby spowodować stratę, oraz funkcję docelową.
Ustalamy funkcję, własność, założenia i wyłączony zakres.
SI przygotowuje kandydatów, a MPK sprawdza certyfikat.
Omawiamy dowód, kontrprzykład, wynik nieustalony, wyłączenia i dowody.
Ustalamy, czy przejść do poprawek, dodatkowych funkcji lub integracji CI/CD.
FAQ
Te odpowiedzi obejmują typowe pytania przed kontaktem, w tym zakres dowodu, rolę SI i sposób obsługi kodu.
Nie. Sprawdzamy wskazaną własność tylko w ramach jawnych założeń, zakresu i obsługiwanego podzbioru Go. Nie daje to gwarancji dla całej aplikacji ani systemów zewnętrznych.
Nie przy pierwszym przeglądzie. Zaczynamy od potwierdzenia funkcji reguł w Go, odizolowanej od zewnętrznego I/O, oraz własności, którą chcecie zagwarantować.
Nie. Gemini tworzy własności, strategie dowodu i kandydatów dowodu. Niezależne jądro MPK akceptuje albo odrzuca końcowy certyfikat.
Klasyfikujemy wynik jako kontrprzykład, nieustalony albo poza zakresem, a potem wyjaśniamy przyczynę, wymagane specyfikacje, prawdopodobne poprawki i sposób wyizolowania jednostki nadającej się do dowodu.
Po potwierdzeniu celu i wykonalności dowodu w przeglądzie gotowości do dowodu możemy osobno zaproponować ciągłe sprawdzanie lub integrację CI/CD.
Nie musicie wklejać poufnego kodu do publicznego formularza. Po zapytaniu potwierdzimy obsługę NDA i bezpieczną metodę udostępniania.
Kontakt
Napisz, która awaria miałaby największe znaczenie i którą funkcję Go mamy przejrzeć. Nie musisz wklejać poufnego kodu do publicznego formularza.
Obsługujemy NDA i bezpieczne udostępnianie kodu