Spec Sharp
Spec# er et programmeringssprog med understøttelse af specifikationssprogfunktioner , der udvider mulighederne for C# programmeringssproget med kontraktprogrammering , som det gøres i Eiffelsproget , herunder objektinvarianter , forudsætninger og postbetingelser. Ligesom ESC/Java indeholder sproget en teorembevisende statisk checker, der gør det muligt at kontrollere de fleste sådanne invarianter statisk. Den indeholder også mange andre mindre tilføjelser, såsom referencetyper, der ikke er nul.
Microsoft Research udviklede både Spec# og C# sprogene . Spec# tjente også som grundlag for skabelsen af Sing# -sproget , også udviklet af Microsoft Research.
Eksempel
Dette eksempel viser to grundlæggende strukturer, der bruges, når du tilføjer kontrakter til din kode.
statisk tomrum Main ( streng ![] args )
kræver args . Length > 0
{
foreach ( string arg in args )
{
Console . WriteLine ( arg );
}
}
- ! bruges til at oprette en ikke-null referencetype, hvilket betyder, at du ikke kan tildele en null-værdi til den. Dette er forskelligt fra null-typer, som gør det muligt at tildele null- værdier til dem .
- kræver ("kræver") betyder en betingelse, der er opfyldt i den givne kode. I dette tilfælde må længden af args ikke være nul eller mindre.
Kilder
- Barnett, M., KRM Leino, W. Schulte, "Spec#-programmeringssystemet: et overblik." Proceedings of Construction og analyse af sikre, sikre og interoperable smarte enheder (CASSIS) , Marseille. Springer Science+Business Media , 2004.
Se også
Yderligere kilder
| Microsoft Research (MSR) |
|---|
Hovedprojekter
_ | |
|---|
| MSR Labs | | Labs | | Faktiske |
- Omdrejningspunkt
- Havdrage
|
|---|
| afbrudt |
- Deepfish
- lister
- Live udklipsholder
- Fotosynth
- Volta
|
|---|
|
|---|
| Labs |
|
|---|
| Andre divisioner |
|
|---|
|
|---|
| Kategori |