Spec Sharp
A Spec# egy olyan programozási nyelv , amely támogatja a specifikációs nyelvi funkciókat , amelyek kiterjesztik a C# programozási nyelv képességeit szerződéses programozással , ahogyan az Eiffel nyelvben is történik , beleértve az objektum invariánsokat , elő- és utófeltételeket. Az ESC/Java -hoz hasonlóan a nyelv tartalmaz egy tételbizonyító statikus ellenőrzőt, amely lehetővé teszi a legtöbb ilyen invariáns statikus ellenőrzését. Számos egyéb kisebb kiegészítést is tartalmaz, például nem nulla hivatkozási típusokat.
A Microsoft Research kifejlesztette a Spec# és a C# nyelveket is . A Spec# szolgált alapul a szintén Microsoft Research által kifejlesztett
Sing# nyelv létrehozásához is.
Példa
Ez a példa két alapvető struktúrát mutat be, amelyeket szerződések kódjához adásakor használnak.
static void Main ( string ![] args )
args szükséges . Length > 0 { foreach ( string arg in args ) { Console . WriteLine ( arg ); } }
- ! nem nulla referenciatípus létrehozására szolgál, ami azt jelenti, hogy nem rendelhet hozzá null értéket. Ez különbözik a null típusoktól, amelyek lehetővé teszik null értékek hozzárendelését .
- megköveteli ("megköveteli") olyan feltételt jelent, amely az adott kódban teljesül. Ebben az esetben az argok hossza nem lehet nulla vagy kisebb.
Források
- Barnett, M., KRM Leino, W. Schulte, "The Spec# Programming System: An Overview." Proceedings of Safe, Secure and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS) , Marseille. Springer Science+Business Media , 2004.
Lásd még
További források
| Microsoft Research (MSR) |
|---|
Főbb
projektek | |
|---|
| MSR Labs | | Labs | | Tényleges |
|
|---|
| megszakított |
- Mélyhal
- listák
- Élő vágólap
- Photosynth
- Volta
|
|---|
|
|---|
| Labs |
|
|---|
| Egyéb osztályok |
|
|---|
|
|---|
| Kategória |