Spec Sharp
Spec# on ohjelmointikieli , joka tukee määrittelykielen ominaisuuksia , jotka laajentavat C# -ohjelmointikielen ominaisuuksia sopimusohjelmoinnilla , kuten se tehdään Eiffel -kielessä , mukaan lukien objektiinvariantit , ennakkoehdot ja jälkiehdot. Kuten ESC/Java , kieli sisältää lauseita todistavan staattisen tarkistimen, jonka avulla useimmat tällaiset invariantit voidaan tarkistaa staattisesti. Se sisältää myös monia muita pieniä lisäyksiä, kuten ei-nolla-viittaustyyppejä.
Microsoft Research kehitti sekä Spec#- että C# -kielet . Spec# toimi myös perustana Sing# -kielen luomiselle, jonka myös Microsoft Research on kehittänyt.
Esimerkki
Tässä esimerkissä esitetään kaksi perusrakennetta, joita käytetään lisättäessä sopimuksia koodiisi.
static void Main ( string ![] args )
vaatii args . Pituus > 0
{
foreach ( string arg in args )
{
Konsoli . WriteLine ( arg );
}
}
- ! käytetään luomaan ei-nolla-viittaustyyppi, mikä tarkoittaa, että sille ei voi määrittää nolla-arvoa. Tämä eroaa nolla-tyypeistä, joiden avulla niille voidaan määrittää nolla -arvoja .
- vaatii ("vaatii") tarkoittaa ehtoa, joka täyttyy annetussa koodissa. Tässä tapauksessa argien pituus ei saa olla nolla tai pienempi.
Lähteet
- Barnett, M., KRM Leino, W. Schulte, "The Spec# Programming System: An Overview." Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS) , Marseilles. Springer Science+Business Media , 2004.
Katso myös
Muita lähteitä
| Microsoft Research (MSR) |
|---|
Pääprojektit
_ | |
|---|
| MSR Labs | | Labs | | Todellinen |
|
|---|
| lopetettu |
- Deepfish
- listat
- Live-leikepöytä
- fotosynth
- Volta
|
|---|
|
|---|
| Labs |
|
|---|
| Muut divisioonat |
|
|---|
|
|---|
| Kategoria |