- /// Function Definition Table syntax:
- ///
- /// - FDT ::= FDTRow [;FDTRow]*
- /// - FDTRow ::= Input => Output | Output <= Input
- /// - Input ::= ParameterName: Value [, Input]*
- /// - Output ::= [ParameterName: Value]* {halt|stop|void|nothing|Value}
- /// - Value ::= true | false | null | notnull | canbenull
- ///
- /// If method has single input parameter, it's name could be omitted.
- /// Using halt (or void/nothing, which is the same) for method output
- /// means that the methos doesn't return normally (throws or terminates the process).
- /// Value canbenull is only applicable for output parameters.
- /// You can use multiple [ContractAnnotation] for each FDT row, or use single attribute
- /// with rows separated by semicolon. There is no notion of order rows, all rows are checked
- /// for applicability and applied per each program state tracked by R# analysis.
- ///
- ///