Abstract This document describes AsmL, a specification language based on abstract state machines. Foundations of Software Engineering Microsoft Research (c) Microsoft Corporation. All rights reserved. Contents 1 Introduction 6
Download 0.93 Mb.
|
- Navigate this page:
- 2.3Values, constructors and patterns
- 2.5.4Datatype declaration
- 2.7Statements and expressions
- 2.7.2Assertion statements
- 2.7.4Return statements return ::= return
- 2.7.6Try/catch expressions
- 2.7.8Selection expressions
- 2.8.2Parallel update blocks
- 2.8.4Exploration expressions
- 2.9.3Delegates delegate ::= delegate
2.2Unit of compilation (assembly)assembly ::= [ namespaceOrDecl ] namespaceOrDecl ::= namespace | declaration namespace ::= [ attributes ] namespace name name ::= id { "." id } declaration ::= import | type | member import ::= import name [ "=" name ] 2.3Values, constructors and patterns2.3.1Constructorsconstructor ::= literal | datatypeConstructor | collectionConstructor datatypeConstructor ::= [ new ] typeName [ "(" [ exps ] ")" ] collectionConstructor ::= tupleExp | setExp | seqExp | mapExp tupleExp ::= "(" exp "," exps ")" setExp ::= "{" [ comprehension | exps | range ] "}" seqExp ::= "[" [ comprehension | exps | range ] "]" mapExp ::= "{" ( mapComprehension | mapExps | "->") "}" range ::= exp ".." exp comprehension ::= exp "|" binders mapComprehension ::= maplet "|" binders mapExps ::= maplet {"," maplet } maplet ::= exp "->" exp 2.3.2Patternspat ::= "_" | literal | id [ as typeExp ] | tuplePat | datatypePat | mapletPat tuplePat ::= "(" pats ")" datatypePat ::= typeName [ "(" [ pats ] ")" ] mapletPat ::= pat "->" pat pats ::= pat { "," pat } 2.3.3Bindersbinders ::= binder {"," binder} binder ::= pat ( in | "=" ) exp [ where exp ] 2.4Type expressionstypeExp ::= optionType { or optionType } optionType ::= atomicType [ "?" ] atomicType ::= typeName | "(" typeExp { "," typeExp } ")" typeName ::= name [ typeArgs ] typeArgs ::= of optionType [ to optionType ] | of "<" typeExp { "," typeExp } ">" 2.5Type declarationstype ::= [ attributes ] { typeModifier } ( class | structure | interface | enum | delegate | constrainedType ) 2.5.1Type ParameterstypeParams ::= of id [ to id ] | of "<" typeParam {"," typeParam } ">" typeParam ::= id [ typeRelations ] 2.5.2Type RelationstypeRelations ::= extends typeExps [ implements typeExps ] | implements typeExps typeExps ::= typeExp { and typeExps } 2.5.3Interfaceinterface ::= interface id [ typeParams ] [ typeRelations ] [ declaration ] 2.5.4Datatype declarationclass ::= [ enumerated ] class id [ typeParams ] [ typeRelations ] [ variantOrDecl ] structure ::= structure id [ typeParams ] [ typeRelations ] [ variantOrDecl ] variantOrDecl ::= declaration | variant variant ::= case id [ declaration ] 2.5.5Enumerationsenum ::= enum id [ extends typeExp ] [ element ] element ::= id [ "=" exp ] 2.5.6Constrained TypesconstrainedType ::= type id [ typeParams ] [ "=" valueExp ] valueExp ::= typeExp [ where exp ] 2.6Membersmember ::= [ attributes ] { memberModifier } ( constant | variable | method | constraint | property | event ) memberModifier ::= shared | virtual | override | extendedMemberModifier 2.6.1Fieldsconstant ::= [ const ] id ( as typeExp [ "=" exp ] | "=" exp ) variable ::= var id ( as typeExp ["=" exp ] | "=" exp ) 2.6.2Methodsmethod ::= [ methodKind ] methodId [ typeParams ] signature [ stm ] methodKind ::= function | procedure methodId ::= name | operator ( binaryOp | unaryOp ) signature ::= params [ result ] result ::= as typeExp params ::= "(" [ param { "," param } ] ")" param ::= [ attributes ] [ paramModifier ] [ id as ] typeExp 2.6.3Constraintsconstraint ::= constraint [ label ] exp label ::= ( id | literal ) ":" 2.7Statements and expressionsstm ::= local | assert | choice | return | operationalStm | exp exp ::= branchExp | exceptExp | quantifierExp | selectExp | binaryExp | enum of type | type of type | do stm | exploration exps ::= exp { "," exp } 2.7.1Local fieldslocal ::= letBinder | { localVariableModifier } localVar letBinder ::= [ let ] pat "=" exp localVar ::= ( var | initially ) id ( as typeExp ["=" exp ] | "=" exp ) 2.7.2Assertion statementsassert ::= constraint | require | ensure require ::= require [ label ] exp ensure ::= ensure [ label ] exp 2.7.3Nondeterministic choice statementschoice ::= choose [ unique ] binders stm [ ifnone stm ] 2.7.4Return statementsreturn ::= return exp 2.7.5Conditional expressionsbranchExp ::= ifExpr | matchExpr ifExpr ::= if exp [ then ] stm { elseif exp [ then ] stm } [ else stm ] matchExp ::= match exp case [ otherwise stm ] case ::= pat [ where exp ] ":" stm 2.7.6Try/catch expressionsexceptExp ::= try stm catch case | throw exp | error exp 2.7.7Quantifying expressionsquantifierExp ::= forall binders holds exp | exists [ unique ] binders 2.7.8Selection expressionsselectExp ::= selector comprehension [ifnone exp] selector ::= any | the | min | max | sum 2.7.9Primary ExpressionsbinaryExp ::= primaryExp { binaryOp primaryExp } primaryExp ::= unaryOp applyExp | applyExp [ ( is | as ) typeExp ] | resulting exp unaryOp ::= not | "-" binaryOp ::= implies | and [ then ] | or [ else ] | "*" | "/" | mod | "+" | "-" | union | intersect | merge | subset | subseteq | in | notin | "=" | "<>" | "<" | ">" | "<=" | ">=" | eq | ne | lt | gt | lte | gte 2.7.10Apply expressionsapplyExp ::= atomicExp { argList } | mybase arglist { argList } argList ::= "(" [ exps ] ")" | "." id [ typeArgs ] } 2.7.11Atomic expressionatomicExp ::= constructor | me | value | "(" exp ")" | id [ typeArgs ] 2.8Runtime statesoperationalStm ::= update | parallelUpdate | sequence | skip 2.8.1Update statementsupdate ::= applyExp ( ":=" | "*=" | "+=" ) exp | add exp to applyExp | remove exp [ from applyExp ] 2.8.2Parallel update blocksparallelUpdate ::= forall binders stm 2.8.3Sequential blockssequence ::= step step ::= step [ label ] [ iterator ] stm iterator ::= foreach binders | for id "=" exp to exp | while exp | until ( exp | fixpoint ) 2.8.4Exploration expressionsexploration ::= explore exp | search exp 2.9.NET Compatibility2.9.1ModifierstypeModifier ::= extensibility | access access ::= public | private | protected | internal extensibility ::= abstract | sealed extendedMemberModifier ::= extensibility | access | primitive paramModifier ::= primitive ref | primitive out | out | inout localVariableModifier ::= primitive 2.9.2Attributesattributes ::= { attribute } attribute ::= "[" [ target ] attributeConstructor { "," attributeConstructor } "]" target ::= id ":" attributeConstructor ::= id | id "(" attributeExps ")" attributeExps ::= [ exps ] [ namedAttrArgs ] namedAttrArgs ::= [ namedAttrArg { "," namedAttrArg } ] namedAttrArg ::= id "=" exp 2.9.3Delegatesdelegate ::= delegate id [ typeParams ] signature 2.9.4Propertiesproperty ::= property ( name | me ) [ params ] as typeExp ( setter [ getter ] | getter [ setter ] ) setter ::= set [ stm ] getter ::= get [ stm ] 2.9.5Eventsevent ::= event name as typeExp ( adder [ remover ] | remover [ adder ] ) adder ::= add [ stm ] remover ::= remove [ stm ] Download 0.93 Mb. Share with your friends:
|