60 lines
1.4 KiB
Plaintext
60 lines
1.4 KiB
Plaintext
[/==============================================================================
|
|
Copyright (C) 2001-2011 Hartmut Kaiser
|
|
Copyright (C) 2001-2011 Joel de Guzman
|
|
|
|
Distributed under the Boost Software License, Version 1.0. (See accompanying
|
|
file LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)
|
|
===============================================================================/]
|
|
|
|
[/------------------------------------------------------------------------------]
|
|
[section XXX]
|
|
|
|
[heading Description]
|
|
|
|
Description of XXX concept
|
|
|
|
[heading Refinement of]
|
|
|
|
[:Link to base concept]
|
|
|
|
[variablelist Notation
|
|
[[`xxx`] [An XXX]]
|
|
]
|
|
|
|
[heading Valid Expressions]
|
|
|
|
(For any XXX the following expressions must be valid:)
|
|
|
|
In addition to the requirements defined in _XXX-Basic_concept_, for any
|
|
XXX the following must be met:
|
|
|
|
[table
|
|
[[Expression] [Semantics] [Return type]]
|
|
[[`xxx`] [Semantics of `xxx`] [XXX]]
|
|
]
|
|
|
|
[heading Type Expressions]
|
|
|
|
[table
|
|
[[Expression] [Description]]
|
|
[[`XXX`] [Description of `XXX`]]
|
|
]
|
|
|
|
[heading Invariants]
|
|
|
|
For any XXX xxx the following invariants always hold:
|
|
|
|
[heading Precondition]
|
|
|
|
Prior to calling FOO the following preconditions should hold:
|
|
|
|
[heading Precondition]
|
|
|
|
Upon return from FOO the following postconditions should hold:
|
|
|
|
[heading Models]
|
|
|
|
Links to models of XXX concept
|
|
|
|
[endsect] [/ XXX Concept]
|