Seite 1 von 1

Wozu PROMELA when man auf plain C schreiben kann?

Verfasst: 24. Okt 2012 12:38
von klte
Hi Leute!

Die drei Zeilen in PROMELA-Sprache sagen viel aus:

c_code {
\#include "someheaders.h"
\#include "someCcode.c"
};

:mrgreen:

Re: Wozu PROMELA when man auf plain C schreiben kann?

Verfasst: 24. Okt 2012 13:12
von yourmaninamsterdam
Man kann das schon machen, aber C-Code wird vom Verifier als korrekt angenommen. Da es hier nicht im Kern um Programmierung, sondern um Modellierung und Verifikation geht, hast du nichts davon, dass Promela embedded C unterstützt. Promela selbst hat andere Kerneigenschaften als C, z. B. Nichtdeterminismus der Ausführung.