1: %

2: % $Id: fse.tex,v 1.10 2002/04/15 22:52:07 kiniry Exp $

3: %

4: 

5: \documentclass{acm_proc_article-sp}[10pt]

6: 

7: \newif\ifpdf

8: \ifx\pdfoutput\undefined

9:    \pdffalse     % no PDFLaTeX

10: \else

11:    \pdfoutput=1  % PDFLaTeX

12:    \pdftrue

13: \fi

14: 

15: \usepackage{times}

16: 

17: \ifpdf

18: \usepackage[pdftex]{graphicx}

19: \else

20: \usepackage{graphicx}

21: \fi

22: 

23: %\usepackage{html}

24: %\usepackage{url}

25: \usepackage{xspace}

26: %\usepackage{doublespace}

27: 

28: \ifpdf

29: \usepackage[pdftex,bookmarks=false,

30:             plainpages=false,naturalnames=true,

31:             colorlinks=true,pdfstartview=FitV,

32:             linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}

33: \else

34: \usepackage[dvips]{hyperref}

35: \fi

36: 

37: \newcommand{\tablesize}{\footnotesize}

38: \newcommand{\eg}{e.g.,\xspace}

39: \newcommand{\ie}{i.e.,\xspace}

40: \newcommand{\etc}{etc.\xspace}

41: 

42: %---------------------------------------------------------------------

43: % New commands, macros, etc.

44: %---------------------------------------------------------------------

45: 

46: % Global

47: 

48: \newcommand{\myhref}[2]{\ifpdf\href{#1}{#2}\else\htmladdnormallinkfoot{#2}{#1}\fi}

49: 

50: \newcommand{\todo}{\textbf{TODO:}}

51: \newcommand{\sksp}{\ensuremath{\;\;\;\;\;}}

52: 

53: \newcommand{\obj}{\footnotesize \begin{alltt}}

54: \newcommand{\jbo}{\end{alltt} \normalsize}

55: 

56: \newcommand{\ms}[1]{{\textit{#1}}}

57: 

58: \newtheorem{Theorem}{Theorem}

59: \newtheorem{Corollary}[Theorem]{Corollary}

60: \newtheorem{Lemma}{Lemma}

61: \newtheorem{Proposition}{Proposition}

62: \newcommand{\Proof}{\nopagebreak\noindent{\textbf{Proof. }}}

63: \newcommand{\ProofOf}[1]{\nopagebreak\noindent{\textbf{Proof of #1}}}

64: \newcommand{\QED}{\hspace*{\fill}\ensuremath{\Box}}

65: %\newtheorem{Proof}{Proof}

66: \newtheorem{Definition}{Definition}

67: \newtheorem{Axiom}{Axiom}

68: \newtheorem{Example}{Example}

69: \newtheorem{Conjecture}{Conjecture}

70: \newtheorem{Fact}{Fact}

71: 

72: \newtheorem{Assumption}{Assumption}

73: \newtheorem{Postulate}{Postulate}

74: 

75: % General rules

76: 

77: \newcommand{\logrule}[2]{\displaystyle \frac{#1}{#2}}

78: 

79: % Introduction

80: 

81: \newcommand{\ITT}{\ensuremath{\mathcal{L}_{0}}}

82: 

83: % Foundations

84: 

85: %

86: \newcommand{\isa}{\ensuremath{<}}

87: \newcommand{\subkind}{\isa}

88: \newcommand{\hasa}{\ensuremath{\supset}}

89: %\newcommand{\equiv}{\ensuremath{\equiv}}

90: \newcommand{\compose}{\ensuremath{\circ}}

91: \newcommand{\prcompose}{\ensuremath{\otimes}}

92: \newcommand{\cocompose}{\ensuremath{\oplus}}

93: \newcommand{\partinterp}{\ensuremath{\hookrightarrow}}

94: \newcommand{\partinterps}[2]{\ensuremath{\overset{#1}{\underset{#2}{\partinterp}}}}

95: \newcommand{\fullinterp}{\ensuremath{\leadsto}}

96: \newcommand{\fullinterps}[2]{\ensuremath{\overset{#1}{\underset{#2}{\fullinterp}}}}

97: \newcommand{\realizes}{\ensuremath{:}}

98: %

99: \newcommand{\dointerpret}{\ensuremath{\hookleftarrow}}

100: \newcommand{\function}{\ensuremath{\rightarrow}}

101: \newcommand{\compute}{\ensuremath{\dashrightarrow}}

102: %

103: \newcommand{\typefont}[1]{\ensuremath{\mathsf{#1}}}

104: \newcommand{\sortfont}[1]{\ensuremath{\mathtt{#1}}}

105: %

106: \newcommand{\setfont}[1]{\ensuremath{\mathit{#1}}}

107: \newcommand{\logimplies}{\ensuremath{\Rightarrow}}

108: \newcommand{\logiff}{\ensuremath{\Leftrightarrow}}

109: \newcommand{\logand}{\ensuremath{\wedge}}

110: \newcommand{\logor}{\ensuremath{\vee}}

111: \newcommand{\setunion}{\ensuremath{\; \cup \;}}

112: \newcommand{\topbot}{\ensuremath{\top, \bot}}

113: \newcommand{\topbotunk}{\ensuremath{\top, \bot, ?}}

114: \newcommand{\emptycontext}{\ensuremath{\varnothing}}

115: \newcommand{\Poset}{\ensuremath{\setfont{Poset}}}

116: \newcommand{\kPoset}{\ensuremath{\knf{Poset}}}

117: %

118: \newcommand{\theoryfont}[1]{\ensuremath{\mathit{#1}}}

119: \newcommand{\KnowledgeTh}{\ensuremath{\theoryfont{ToK}}}

120: \newcommand{\AlgKT}{\ensuremath{\theoryfont{AlgKT}}}

121: \newcommand{\MaudeKT}{\ensuremath{\theoryfont{MaudeKT}}}

122: \newcommand{\HyperKT}{\ensuremath{\theoryfont{HyperKT}}}

123: \newcommand{\MDKT}{\ensuremath{\theoryfont{MDKT}}}

124: \newcommand{\KindKT}{\ensuremath{\theoryfont{KindKT}}}

125: %

126: \newcommand{\kindfont}[1]{\ensuremath{\mathbb{#1}}}

127: \newcommand{\Universe}{\ensuremath{\kindfont{U}}}

128: \newcommand{\Data}{\ensuremath{\kindfont{D}}}

129: \newcommand{\Behavior}{\ensuremath{\kindfont{B}}}

130: \newcommand{\Bool}{\ensuremath{\kindfont{2}}}

131: \newcommand{\Predicate}{\ensuremath{\kindfont{P}}}

132: \newcommand{\Agent}{\ensuremath{\kindfont{A}}}

133: \newcommand{\Evidence}{\ensuremath{\kindfont{E}}}

134: \newcommand{\Context}{\ensuremath{\kindfont{C}}}

135: \newcommand{\Instance}{\ensuremath{\kindfont{I}}}

136: \newcommand{\Kind}{\ensuremath{\kindfont{K}}}

137: \newcommand{\Tri}{\ensuremath{\kindfont{3}}}

138: %

139: \newcommand{\subcategory}{\ensuremath{\subset}}

140: \newcommand{\fullsubcategory}{\ensuremath{\subseteq}}

141: \newcommand{\coproduct}{\ensuremath{+}}

142: \newcommand{\product}{\ensuremath{\times}}

143: \newcommand{\arrow}{\ensuremath{\rightarrow}}

144: \newcommand{\longarrow}[1]{\ensuremath{\xrightarrow{#1}}}

145: %

146: \newcommand{\topmorph}{\ensuremath{\vartriangle}}

147: \newcommand{\groundmorph}{\ensuremath{\nabla}}

148: \newcommand{\Top}{\ensuremath{\kindfont{P}}}

149: \newcommand{\topelement}{\ensuremath{\aleph}}

150: %

151: \newcommand{\Cat}[1]{\ensuremath{\boldsymbol{#1}}}

152: \newcommand{\Obj}[1]{\ensuremath{Obj(#1)}}

153: \newcommand{\Arrows}[1]{\ensuremath{Arrows(#1)}}

154: \newcommand{\CPoset}{\ensuremath{\Cat{Poset}}}

155: \newcommand{\CContainers}{\ensuremath{\Cat{Containers}}}

156: \newcommand{\CSKind}{\ensuremath{\Cat{Single}}}

157: \newcommand{\CMKind}{\ensuremath{\Cat{Multi}}}

158: \newcommand{\CMEquiv}{\ensuremath{\Cat{Equiv}}}

159: \newcommand{\CData}{\ensuremath{\Cat{Data}}}

160: \newcommand{\CBehavior}{\ensuremath{\Cat{Behavior}}}

161: \newcommand{\CKind}{\ensuremath{\Cat{Kind}}}

162: %

163: \newcommand{\CSpec}{\ensuremath{\Cat{Spec}}}

164: \newcommand{\CAlg}{\ensuremath{\Cat{Alg}}}

165: \newcommand{\CMaude}{\ensuremath{\Cat{Maude}}}

166: \newcommand{\CHyper}{\ensuremath{\Cat{Hyper}}}

167: %

168: \newcommand{\modelfont}[1]{\ensuremath{\mathcal{#1}}}

169: %

170: \newcommand{\ClaimMap}{\ensuremath{\gamma}}

171: \newcommand{\BeliefMap}{\ensuremath{\beta}}

172: \newcommand{\BInterpretMap}{\ensuremath{\xi}}

173: \newcommand{\DInterpretMap}{\ensuremath{\zeta}}

174: \newcommand{\RealizationMap}{\ensuremath{\rho}}

175: \newcommand{\ContextChangeFunctor}{\ensuremath{\Delta}}

176: \newcommand{\JudgmentMap}{\ensuremath{\vDash}}

177: \newcommand{\JudgmentMapF}[2]{\ensuremath{\overset{#1}{\underset{#2}{\JudgmentMap}}}}

178: %

179: \newcommand{\DataSet}{\ensuremath{D}}

180: \newcommand{\BehaviorSet}{\ensuremath{B}}

181: \newcommand{\InterpretSet}{\ensuremath{\boldsymbol{\Xi}}}

182: \newcommand{\ModelSet}{\ensuremath{\boldsymbol{\modelfont{M}}}}

183: \newcommand{\ToK}[3]{\ensuremath{\langle{}#1,#2,#3\rangle}}

184: %

185: \newcommand{\kindnamefont}[1]{\textsc{#1}}

186: \newcommand{\knf}[1]{\kindnamefont{#1}}

187: \newcommand{\instancenamefont}[1]{\ensuremath{\textrm{#1}}}

188: 

189: % Kind Theory

190: 

191: \newcommand{\KT}{\ensuremath{\theoryfont{KT}}}

192: \newcommand{\PL}{\ensuremath{\theoryfont{L}}}

193: \newcommand{\Gentzen}{\ensuremath{\theoryfont{LK'}}}

194: \newcommand{\CFK}{\textsc{CFK}}

195: \newcommand{\KcoL}{\ensuremath{K \cocompose L}}

196: \newcommand{\McoN}{\ensuremath{M \cocompose N}}

197: \newcommand{\KprL}{\ensuremath{K \prcompose L}}

198: \newcommand{\MprN}{\ensuremath{M \prcompose N}}

199: 

200: % contexts

201: \newcommand{\gamv}{\ensuremath{\Gamma \vdash}}

202: \newcommand{\gamav}{\ensuremath{\Gamma,A \vdash}}

203: \newcommand{\gamm}{\ensuremath{\Gamma \vDash}}

204: \newcommand{\gamam}{\ensuremath{\Gamma,A \vDash}}

205: \newcommand{\unk}{\ensuremath{?}}

206: % agent, predicate, evidence

207: \newcommand{\claim}[3]{\ensuremath{\ClaimMap_{#1}(#2|#3)}}

208: % agent, predicate, evidence, degree

209: \newcommand{\belief}[4]{\ensuremath{\BeliefMap_{#1}(#2|#3)=#4}}

210: % agent, predicate, no evidence, degree

211: \newcommand{\beliefshort}[3]{\ensuremath{\BeliefMap_{#1}(#2|)=#3}}

212: 

213: % core functional kind

214: \newcommand{\parent}{\ensuremath{\isa_{p}}}

215: \newcommand{\partof}{\ensuremath{\subset_{p}}}

216: \newcommand{\canon}{\ensuremath{[]}}

217: \newcommand{\canonform}[1]{\ensuremath{[#1]}}

218: \newcommand{\equival}[1]{\ensuremath{\equiv_{#1}}}

219: \newcommand{\equivalclass}[2]{\ensuremath{[#1]_{#2}}}

220: \newcommand{\equals}{\ensuremath{=}}

221: \newcommand{\fullequiv}{\ensuremath{\eqcirc}}

222: \newcommand{\partequiv}{\ensuremath{\lessdot}}

223: \newcommand{\fullequival}[1]{\ensuremath{\fullequiv_{#1}}}

224: \newcommand{\partequival}[1]{\ensuremath{\partequiv_{#1}}}

225: \newcommand{\isakindof}{\ensuremath{\isa_{r}}}

226: % functional form of prcompose is product and cocompose is coproduct.

227: \newcommand{\follows}{\ensuremath{\cdotp}}

228: 

229: % Kind Type Theory

230: 

231: \newcommand{\Fone}{\ensuremath{F_{1}}}

232: \newcommand{\Fones}{\ensuremath{F_{1<:}}}

233: \newcommand{\Ftwo}{\ensuremath{F_{2}}}

234: \newcommand{\groundS}{\ensuremath{S_G}}

235: \newcommand{\sigBT}{\ensuremath{\Sigma_{\texttt{BT}}}}

236: \newcommand{\coreA}{\ensuremath{T_{\sigBT}}}

237: \newcommand{\listA}{\ensuremath{T_{\Sigma_{\texttt{List}}}}}

238: \newcommand{\listAG}{\ensuremath{T_{\Sigma_{\texttt{List[Ground]}}}}}

239: \newcommand{\listAS}{\ensuremath{T_{\Sigma_{\texttt{List[Slot]}}}}}

240: \newcommand{\typeA}{\ensuremath{T_{\Sigma_T}}}

241: \newcommand{\instanceA}{\ensuremath{T_{\Sigma_I}}}

242: \newcommand{\termA}{\ensuremath{T_{0}}}

243: \newcommand{\contextA}{\ensuremath{T_\Gamma}}

244: \newcommand{\kttA}{\ensuremath{A_\mathcal{T}}}

245: \newcommand{\gam}{\ensuremath{\Gamma}}

246: \newcommand{\gamT}{\ensuremath{\Gamma_T}}

247: \newcommand{\gamTv}{\ensuremath{\Gamma_T \vdash}}

248: \newcommand{\gamTp}{\ensuremath{{\Gamma_{T}}'}}

249: \newcommand{\gamTpv}{\ensuremath{{\Gamma_{T}}' \vdash}}

250: \newcommand{\gamI}{\ensuremath{\Gamma_I}}

251: \newcommand{\gamIv}{\ensuremath{\Gamma_I \vdash}}

252: \newcommand{\gamIpv}{\ensuremath{\Gamma_I' \vdash}}

253: \newcommand{\gamTI}{\ensuremath{\gamT \triangleright \gamI}}

254: \newcommand{\gamTIv}{\ensuremath{\gamT \triangleright \gamIv}}

255: \newcommand{\typicaltype}{\ensuremath{\langle N,\{T\},\{S\} \rangle}}

256: \newcommand{\typicaltypep}{\ensuremath{\langle N',\{T'\},\{S'\} \rangle}}

257: \newcommand{\typicaltypepp}{\ensuremath{\langle N'',\{T''\},\{S''\} \rangle}}

258: \newcommand{\typicalinst}{\ensuremath{\langle I,T,\{V\} \rangle}}

259: \newcommand{\typicalinstp}{\ensuremath{\langle I',T',\{V'\} \rangle}}

260: \newcommand{\wff}{\ensuremath{\vdash \diamond}}

261: 

262: % Reflect

263: 

264: % basic constructs

265: \newcommand{\kUniv}{\knf{Universal}}

266: \newcommand{\kConstruct}{\knf{Construct}}

267: \newcommand{\kAsset}{\knf{Asset}}

268: \newcommand{\kKind}{\knf{Kind}}

269: \newcommand{\kInstance}{\knf{Instance}}

270: \newcommand{\kKKxII}{\knf{K\arrow{}K\product{}I\arrow{}I}}

271: \newcommand{\kContext}{\knf{Context}}

272: \newcommand{\kDomain}{\knf{Domain}}

273: \newcommand{\kBehavior}{\knf{Behavior}}

274: \newcommand{\kData}{\knf{Data}}

275: \newcommand{\kAgent}{\knf{Agent}}

276: \newcommand{\kFunction}{\knf{Function}}

277: \newcommand{\kRelation}{\knf{Relation}}

278: \newcommand{\kPredicate}{\knf{Predicate}}

279: \newcommand{\kEvidence}{\knf{Evidence}}

280: % supp structures

281: \newcommand{\kColl}{\knf{Collection}}

282: \newcommand{\kSet}{\knf{Set}}

283: \newcommand{\kList}{\knf{List}}

284: \newcommand{\kBag}{\knf{Bag}}

285: % supp notions

286: \newcommand{\kFDomain}{\knf{FunctionDomain}}

287: \newcommand{\kFCodomain}{\knf{FunctionCodomain}}

288: \newcommand{\kRCodomain}{\knf{RelationCodomain}}

289: % basic functions and relations

290: \newcommand{\kInherit}{\knf{Inheritance}}

291: \newcommand{\kParent}{\knf{Parent}}

292: \newcommand{\kInc}{\knf{Inclusion}}

293: \newcommand{\kComp}{\knf{Composition}}

294: \newcommand{\kPrComp}{\knf{ProductComposition}}

295: \newcommand{\kCoComp}{\knf{CoproductComposition}}

296: \newcommand{\kEquiv}{\knf{Equivalence}}

297: \newcommand{\kEqual}{\knf{Equality}}

298: \newcommand{\kReal}{\knf{Realization}}

299: \newcommand{\kInterp}{\knf{Interpretation}}

300: \newcommand{\kPartInterp}{\knf{PartialInterpretation}}

301: \newcommand{\kFullInterp}{\knf{FullInterpretation}}

302: \newcommand{\kCompute}{\knf{Computation}}

303: % interpretation-related kind

304: \newcommand{\kCFunction}{\knf{ClassificationFunction}}

305: \newcommand{\kDInterp}{\knf{DataInterpretation}}

306: \newcommand{\kBInterp}{\knf{BehaviorInterpretation}}

307: % standard grounds

308: \newcommand{\kBTV}{\knf{BooleanTruthValues}}

309: \newcommand{\kBool}{\knf{Boolean}}

310: \newcommand{\kInt}{\knf{Integer}}

311: \newcommand{\kFloat}{\knf{Float}}

312: \newcommand{\kString}{\knf{String}}

313: % alternative/supp grounds

314: \newcommand{\kTri}{\knf{Tri}}

315: \newcommand{\kTTV}{\knf{TernaryTruthValues}}

316: \newcommand{\kR}{\knf{Real}}

317: % mathematical terms

318: \newcommand{\kVoM}{\knf{VocabularyOfMathematics}}

319: \newcommand{\kMT}{\knf{MathematicalTerm}}

320: %

321: \newcommand{\kDefinition}{\knf{Definition}}

322: \newcommand{\kFact}{\knf{Fact}}

323: \newcommand{\kAxiom}{\knf{Axiom}}

324: \newcommand{\kTheorem}{\knf{Theorem}}

325: \newcommand{\kLemma}{\knf{Lemma}}

326: \newcommand{\kCorollary}{\knf{Corollary}}

327: \newcommand{\kConjecture}{\knf{Conjecture}}

328: \newcommand{\kProof}{\knf{Proof}}

329: \newcommand{\kProposition}{\knf{Proposition}}

330: \newcommand{\kTerm}{\knf{Term}}

331: \newcommand{\kVariable}{\knf{Sentence}}

332: \newcommand{\kSentence}{\knf{Sentence}}

333: \newcommand{\kFormula}{\knf{Formula}}

334: % mathematics

335: \newcommand{\kTheory}{\knf{Theory}}

336: \newcommand{\kLogic}{\knf{Logic}}

337: \newcommand{\kAlgebra}{\knf{Algebra}}

338: \newcommand{\kCalculus}{\knf{Calculus}}

339: 

340: % Motivating Example

341: \newcommand{\kLoop}{\knf{Loop}}

342: \newcommand{\kFMLoop}{\knf{FormalLoop}}

343: \newcommand{\kLoopSpec}{\knf{LoopSpecification}}

344: 

345: %=====================================================================

346: 

347: \begin{document}

348: 

349: % --- Author Metadata here ---

350: \conferenceinfo{FSE-10}{2002 Charleston, South Carolina, USA}

351: %\setpagenumber{50}

352: \CopyrightYear{2002}

353: %\crdata{0-12345-67-8/90/01}  % Allows default copyright data (0-89791-88-6/97/05) to be over-ridden - IF NEED BE.

354: % --- End of Author Metadata ---

355: 

356: \title{Semantic Properties for Lightweight Specification in \\

357:   Knowledgeable Development Environments}

358: \numberofauthors{1}

359: \author{

360: \alignauthor Joseph R.~Kiniry\\

361:        \affaddr{Department of Computer Science}\\

362:        \affaddr{California Institute of Technology}\\

363:        \affaddr{Mailstop 256-80}\\

364:        \affaddr{Pasadena, CA 91125}\\

365:        \email{kiniry@acm.org}

366: }

367: 

368: \maketitle

369: 

370: %======================================================================

371: \begin{abstract}

372:   

373:   Semantic properties are domain-specific specification constructs used to

374:   augment an existing language with richer semantics.  These properties are

375:   taken advantage of in system analysis, design, implementation, testing,

376:   and maintenance through the use of documentation and source-code

377:   transformation tools.  Semantic properties are themselves specified at

378:   two levels: loosely with precise natural language, and formally within

379:   the problem domain.  The refinement relationships between these

380:   specification levels, as well as between a semantic property's use and

381:   its realization in program code via tools, is specified with a new formal

382:   method for reuse called kind theory.

383:   

384: \end{abstract}

385: 

386: % TODO: replace augment throughout.  Replace use of ``We have''.

387: 

388: %=====================================================================

389: % A category with only the three required fields

390: \category{D.1.0}{Software}

391:                 {Programming Techniques}

392:                 [General]

393: \category{D.2}{Software}

394:               {Software Engineering}

395: %\category{D.2.1}{Software}

396: %                {Software Engineering}

397: %                {Requirements/Specifications}

398: %                [Languages, Methodologies, Tools]

399: %\category{D.2.2}{Software}

400: %                {Software Engineering}

401: %                {Design Tools and Techniques}

402: %\category{D.2.2}{Software}

403: %                {Software Engineering}

404: %                {Coding Tools and Techniques}

405: %                [Object-oriented programming, Program editors]

406: %\category{D.2.4}{Software}

407: %                {Software Engineering}

408: %                {Software/Program Verification}

409: %\category{D.2.5}{Software}

410: %                {Software Engineering}

411: %                {Testing and Debugging}

412: %\category{D.2.6}{Software}

413: %                {Software Engineering}

414: %                {Programming Environments}

415: %\category{D.2.7}{Software}

416: %                {Software Engineering}

417: %                {Distribution, Maintenance, and Enhancement}

418: %                [Documentation]

419: %\category{D.2.10}{Software}

420: %                 {Software Engineering}

421: %                 {Design}

422: %\category{D.2.13}{Software}

423: %                 {Software Engineering}

424: %                 {Reusable Software}

425: \category{D.3.1}{Software}

426:                 {Programming Languages}

427:                 [Formal Definitions and Theory]

428: \category{D.3.2}{Software}

429:                 {Programming Languages}

430:                 [Language Classifications]

431:                 [design languages]

432: \category{D.3.4}{Software}

433:                 {Programming Languages}

434:                 [Processors]

435:                 [preprocessors]

436: \category{F.3.1}{Theory of Computation}

437:                 {Logics and Meanings of Programs}

438:                 [Specifying and Verifying and Reasoning about Programs]

439: \category{F.4.1}{Theory of Computation}

440:                 {Mathematical Logic and Formal Languages}

441:                 [Mathematical Logic]

442: \category{F.4.3}{Theory of Computation}

443:                 {Mathematical Logic and Formal Languages}

444:                 [Formal Languages]

445:                 

446:                 \terms{documentation, semantic properties, specification

447:                   languages, formal methods, kind theory, specification

448:                   reuse, documentation reuse}

449: 

450: %=====================================================================

451: % Introduction stating precisely the problem addressed in the paper. 

452: %=====================================================================

453: \vspace{1in}

454: 

455: \section{Introduction}

456: \label{sec:introduction}

457: 

458: Ad hoc constructs and local conventions have been used to annotate program

459: code since the invention of programming languages.  The purpose of these

460: annotations is to convey extra programmer knowledge to other system

461: developers and future maintainers.  These comments usually fall into that

462: gray region between completely unstructured natural language and formal

463: specification.

464: 

465: Invariably, such program comments rapidly exhibit ``bit rot''.  Over time,

466: these comments, unless well maintained by documentation specialists,

467: rigorous process, or other extra-mile development efforts, become

468: out-of-date.  They are the focus for the common mantra: an incorrect

469: comment is worse than no comment at all.

470: 

471: Recently, with the adoption and popularization of light\-weight

472: documentation tools in the literate programming tradition~\cite{Knuth92,

473:   KnuthLevy93}, an ecology of semi-structured comments is flourishing.  The

474: rapid adoption and popularity of Java primed interest in semi-structured

475: comment use via the Javadoc tool.  Other similar code-to-documentation

476: transformation tools have since followed in volume including Jakarta's

477: Alexandria, Doxygen, and Apple's HeaderDoc.

478: \myhref{http://www.sf.net/}{Source\-Forge} reports thirty-six projects with

479: ``Javadoc'' in the project summary.

480: \myhref{http://www.freshmeat.net/}{Fresh\-Meat} reports another

481: thirty-five, with some overlap.

482: 

483: While most of these systems are significantly more simple than Knuth's

484: original CWEB, they share two key features.  

485: 

486: First, they are easy to learn, since they necessitate only a small change

487: in \emph{convention} and \emph{process}.  Rather than forcing the

488: programmer to learn a new language, complex tool, or imposing some other

489: significant barrier to use, these tools actually \emph{reward} the

490: programmer for documenting her code.  

491: 

492: Second, a culture of documentation is engendered.  Prompted by the example

493: of vendors like Sun, programmers enjoy the creation and use of the

494: attractive automatically-generated documentation in a web page format.

495: This documentation-centric style is only strengthened by the exhibitionist

496: nature of the Web.  Having the most complete documentation is now a point

497: of pride in some Open Source projects; a state of affairs we would not have

498: guessed at a decade ago.

499: 

500: The primary problem with these systems, and the documentation and code

501: written using them, is that \emph{even semi-structured comments have no

502:   semantics}.  Programmers are attempting to state (sometimes quite

503: complex) knowledge but are not given the language and tools with which to

504: communicate this knowledge.  And since the vast majority of developers are

505: unwilling to learn a new, especially formal, language with which to convey

506: such information, we must look for a happy-medium of \emph{informal

507:   formality}.

508: 

509: That compromise, the delicate balance between informality and formality,

510: and the lightest-weight aspect of our \emph{Knowledgeable Software

511:   Engineering} program, is what we call \emph{semantic properties}.

512: 

513: Semantic properties are domain-independent documentation constructs with

514: intuitive formal semantics that are mapped into the semantic domain of

515: their application.  Semantic properties are used as if they were normal

516: semi-structured documentation. But, rather than being ignored by compilers

517: and development environments as comments typically are, they have the

518: attention of augmented versions of such tools.  Semantic properties embed

519: a tremendous amount of concise information wherever they are used without

520: imposing the often insurmountable overhead seen in the introduction of new

521: languages and formalisms for similar purposes.

522: 

523: %=====================================================================

524: \section{Semantic Properties}

525: \label{sec:semantic-properties}

526: 

527: The original inspiration for semantic properties came from three sources:

528: the use of tags, (e.g., \texttt{@author} and \texttt{@param}), in the

529: Javadoc system, the use of annotations and pragmas in languages like Java

530: and C for code transformation and guided compilation, and indexing clauses

531: in Eiffel.  All of these systems have a built-in property-value mechanism,

532: one at the documentation level and one within the language syntax itself,

533: that is used to specify semi-structured information.

534: 

535: In Java, tags are the basic realization of our semantic properties.  They

536: are used for documentation and formal specification, as we will discuss in

537: more detail in Section~\ref{sec:java}.  Tags are not part of the language

538: specification.  In fact, they are entirely ignored by all Java compilers.

539: 

540: Annotations and pragmas come in the form of formal tags used for some

541: Design by Contract tools like

542: \myhref{http://semantik.informatik.uni-oldenburg.de/~jass/}{Jass} which

543: happen to be realized in Eiffel with first-class keywords like

544: \emph{require}, \emph{ensure}, and \emph{invariant}.

545: 

546: Eiffel provides first-class support for properties via \emph{indexing

547:   clauses}.  An Eiffel file can contain arbitrary property-value pairs

548: inside of \texttt{indexing} blocks.  This information is used by a variety

549: of tools for source code search, organization, and documentation.

550: 

551: \vspace{0.5in}

552: 

553: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

554: \subsection{Documentation Semantics}

555: \label{sec:docum-semant}

556: 

557: Recently, Sun has started to extend the semantics of these basic properties

558: with respect to language semantics, particularly with regards to

559: inheritance.  If a class $C$ inherits from a parent class $P$, and $P$'s

560: method $m$ has some documentation, but $C$'s overridden or effective (in

561: the case where $P$ and/or $m$ is \emph{abstract}) version of $m$ does not,

562: then Javadoc \emph{inherits} $C.m$'s documentation for $P.m$, generating

563: the appropriate comments in Javadoc's output.

564: 

565: This change in behavior of the tools is an implicit change in the semantics

566: of the documentation.  While straightforward and useful in this example,

567: the meaning of such inheritance is undocumented and often unclear.

568: 

569: The situation in Eiffel is less confusing.  The semantics of properties, as

570: realized by indexing clauses and formal program annotation via contracts,

571: are defined in the language standard~\cite{Meyer90-ETL}.  

572: 

573: Even so, no mechanism exists in either system for extending these

574: semi-structured comments with new semantics beyond simple plug-ins for

575: documentation (e.g., doclets in Java and translators in EiffelStudio).

576: 

577: Also, the semantics of current annotations are entirely specified within a

578: particular language or formalism.  No general purpose formalism has been

579: used to express their extra-model semantics.

580: 

581: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

582: \subsection{Semantics of Semantic Properties}

583: \label{sec:semant-semant-prop}

584: 

585: We specify the semantics of semantic properties in a new formalism called

586: \emph{kind theory}.  Kind theory is a logic used to describe, reason about,

587: and discover reusable assets of arbitrary sorts.  Kind theory is an

588: higher-order, autoepistemic\footnote{Auto-epistemic: ``representing or

589:   discussing self-knowledge''.}, paraconsistent\footnote{Paraconsistent:

590:   ``explicitly representing and reasoning with potential and transitory

591:   logic inconsistency''.}, categorical logic with a type theoretic and

592: algebraic model, and is described in full detail in Kiniry's

593: dissertation~\cite{Kiniry02-PhD}.

594: 

595: %---------------------------------------------------------------------

596: \subsubsection{A Brief Overview of Kind Theory}

597: \label{sec:brief-overview-kind}

598: 

599: \emph{Kind} are classifiers used to describe reusable assets like program

600: code, components, documentation, specifications, etc. \emph{Instances} are

601: realizations of kind---actual embodiments of these classifiers.  For

602: example, the paperback ``The Portrait of the Artist as a Young Man'' by

603: James Joyce is an \emph{instance} of \emph{kinds} $\knf{PaperbackBook}$,

604: $\knf{EnglishDocument}$, and others.

605: 

606: In the context of semantic properties, our kinds are the semantic

607: properties as well as the programming language constructs to which the

608: properties are bound.  Our instances are the specific realizations of these

609: kinds within a particular input structure, typically a programming or

610: specification language.

611: 

612: Kinds are described structurally using our logic in a number of ways.

613: Classification is covered with the inheritance operators $\isa$ and

614: $\parent$; structural relationships are formalized using the inclusion

615: operators $\partof$ and $\hasa$, equivalence has several forms $\fullequiv$

616: and $\partequiv$; realization, the relationship between instances and kind,

617: is formalized with the operators $\isakindof$ and $\realizes$; composition

618: is captured in several forms, $\prcompose$, $\cocompose$, and $\compose$;

619: and interpretation, the translation of kind to kind or instances to

620: instances, is realized with the operators $\partinterp$ and $\fullinterp$.

621: 

622: Semantics are specified in an autoepistemic fashion using what are called

623: \emph{truth structures}.  Truth structures come in two forms:

624: \emph{claims} and \emph{beliefs}.

625: 

626: \emph{Claims} are stronger than beliefs.  A mathematically proven statement

627: that is widely accepted is a claim.  This phrasing is used because, for

628: example, there are theorems that have a preliminary proof but are not yet

629: widely recognized as being true.

630: 

631: A statement that is universally accepted, but not necessarily

632: mathematically proven, is also a claim.  Claims are not necessarily

633: mathematical formulas.  The statement ``the sun will rise tomorrow'' is

634: considered by the vast majority of listeners a true and valid statement,

635: thus is classified as a claim rather than as a belief.

636: 

637: \emph{Beliefs}, on the other hand, range in surety from \emph{completely

638:   unsure} to \emph{absolutely convinced}.  No specific metric is defined

639: for the degree of conviction, the only requirement placed on the associated

640: belief logic is that the belief degree form a partial order.

641: 

642: We use kind theory to specify semantic properties because it provides us

643: with an excellent model-independent (i.e., it is not bound to some specific

644: programming language) reuse-centric formalism.  Kind theory's whole

645: purpose is the specification of such reusable concepts.

646: 

647: We have insufficient space to summarize kind theory here, so we will simply

648: provide some basic definitions, examples, and motivation of its use within

649: the context of semantic properties.

650: 

651: %---------------------------------------------------------------------

652: \subsubsection{Kind Theory and Semantic Properties}

653: \label{sec:kind-theory-semantic}

654: 

655: Using kind theory, we specify the semantic relationships between

656: specifications and their realization.  With regards to semantic properties,

657: these relation\-ships formally explain which properties exist, how they can

658: be structured, how they can be applied in a specific language or system,

659: and how they are interpreted into alternative forms like documentation and

660: test code.

661: 

662: First, we denote the classification relationships between kinds using

663: inheritance operators.  Properties are classified using standard conceptual

664: data modeling~\cite{HerzigGogolla92, Wille97} and onto\-logy

665: en\-gin\-eer\-ing~\cite{Bench-CaponMalcolm99, Gruber00, VandervetMars98}

666: techniques into a kind hierarchy.  Details about these classifications for

667: semantic properties are discussed in Section~\ref{sec:prop-class}.

668: 

669: Next, the structural relationships between kinds are specified using the

670: inclusion operators.  Structural relationship denote the contexts in which

671: a kind can be used and how kinds are composed to create new kinds.  We

672: discuss structural relations in more detail in Section~\ref{sec:context}.

673: 

674: Finally, equivalence relations and interpretations are defined on kinds.

675: Equivalence relations help refine concepts embodied as kinds for particular

676: domain models by folding and simplifying kind hierarchies.  They also let

677: the user pick representative structures, called \emph{canonical forms},

678: that are used to represent and reason about (semi-)equivalent kind.

679: 

680: Interpretations, which are structure-preserving functions, are defined to

681: help capture notions of inheritance, equivalence, and other inter-domain

682: translations.

683: 

684: The formal aspects of kind theory, the specification of kind domains for

685: things like semantic properties, is performed by an expert.  The typical

686: software engineer never needs to learn or witness the formalism to benefit

687: from its availability.

688: 

689: \paragraph{A Kind Example}

690: Consider a loop in any standard programming language.  Loops come in many

691: syntactic forms.  For example, in the C programming language there are

692: three primary loop constructs: \texttt{for}, \texttt{while}, and

693: \texttt{do}.  Fundamentally, all loop constructs are equivalent to each

694: other at some abstraction level; they are each just syntactic variations on

695: a common theme.  That theme is specified by the kind $\kLoop$.  

696: 

697: We classify loops as a computational structure.  This classification states

698: that the notion of a loop is going to be bound to a specific syntax and can

699: be interpreted in some programmatic context.  We state this relation as

700:                $$\kLoop \isa \knf{ComputationalStructure}$$

701: By the rules of inheritance, all the structure inherent in the

702: parent kind, that of $\knf{ComputationalStructure}$, is realized in the

703: child kind $\kLoop$ as well.

704: 

705: Additionally, an interpretation exists of the form

706:             $$\kLoop \partinterp \knf{ComputationalStructure}$$

707: that takes kinds or instances of loops to kinds or instances of

708: computational structures, respectively.  This function is called a

709: \emph{partial interpretation} because it eliminates all of the semantics of

710: loops that differentiates them from general computational structures.

711: Interpretations are realized by categorical forgetful functors in kind

712: theory.

713: 

714: The structure of loops is straightforward.  Each loop has an initial state,

715: an increment function, a guard, and a body.  We state this kind

716: theoretically as

717: \begin{gather*}

718:   \knf{InitialState} \partof \kLoop \\

719:   \knf{IncrementFunction} \partof \kLoop \\

720:   \knf{GuardPredicate} \partof \kLoop \\

721:   \knf{LoopBody} \partof \kLoop

722: \end{gather*}

723: Each of these kind, in turn, has its own structure associated with it.

724: $\knf{GuardPredicate} \isa \knf{Predicate}$, for example.

725: 

726: Interpretations let us do two primary things.  First, we use

727: interpretations to translate among different forms of loops, converting a

728: \texttt{while} loop into a \texttt{do} loop, for example.  Second, they are

729: used for interpreting the generic semantics of loops in a specific language

730: or formal context.

731: 

732: For instance, a generic specification of a loop instance can be translated

733: to and from a specific syntactic structure realized in the Java programming

734: language.  Additionally, a formally specified loop, (the kind

735: $\knf{FormalLoop}$), complete with a loop variant function and invariant

736: predicate, can be translated into a proof structure in our logical

737: framework.  This opens up the opportunity for statically proving the

738: correctness of such formally specified loops.

739: 

740: All of the above details are fully formalized in a \emph{kind domain} in

741: the basic kind system~\cite{Kiniry02-PhD}.

742: 

743: A \emph{kind domain} is simply a set of kind and instances that are

744: specific to some domain of knowledge.  In this case, that domain is one of

745: language-generic computational structures, and we call that domain

746: $\knf{ComputationalStructures}$.

747: 

748: A \emph{kind system} is an actual computational system that realizes kind

749: theory.  Our first realization is witnessed both in a logical framework,

750: that of SRI's Maude~\cite{ClavelDuranEtal99-Metatool}, as well as in

751: software engineering tools like the \myhref{http://www.jiki.org/}{Jiki}

752: (used as an open, collaborative knowledge repository), the

753: JPP~\cite{KiniryCheong98}, and the \myhref{http://ebon.sf.net/}{EBON tool

754:   suite} (a design model checker).  Some of these tools are discussed in

755: more detail in

756: Sections~\ref{sec:tool-support}~and~\ref{sec:embedd-semant-prop}.

757: 

758: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

759: \subsection{Properties and Their Classification}

760: \label{sec:prop-class}

761: 

762: We have defined elsewhere\footnote{The original specification of these

763:   properties was in the Infospheres Java Coding Standard

764:   (\href{http://www.infospheres.caltech.edu/})

765:   {http://www.infospheres.caltech.edu/}.  That standard has since been

766:   refined and broadened.  More recent versions are available at

767:   KindSoftware (\href{http://www.kindsoftware.com/}

768:   {http://www.kindsoftware.com/}).}  thirty-five semantic properties.  All

769: semantic properties are enumerated in

770: Table~\ref{tab:The_Full_Set_of_Semantic_Properties} in the appendix.  Since

771: we have only a limited amount of space in this paper, we will summarize

772: some of the more interesting properties, their semantics, and our

773: experiences with their use in a number of software engineering projects,

774: large and small, over the last five years.

775: 

776: To derive our core set of semantic properties, we abstracted and unified

777: the existing realizations that we have used in two languages for many

778: years.  First, we gathered the set of predefined Javadoc tags, the standard

779: Eiffel indexing clauses, and the set of basic formal specification

780: constructs.  After that set was made self-consistent, that is, duplicates

781: were removed, semantics were weakened across domains for the

782: generalization, etc., we declared it the \emph{core set} of semantic

783: property kind.

784: 

785: These properties were then classified according to their general use and

786: intent.  The classifications are: \emph{meta-information}, \emph{pending

787:   work}, \emph{contracts}, \emph{concurrency}, \emph{usage information},

788: \emph{versioning}, \emph{inheritance}, \emph{documentation},

789: \emph{dependencies}, and \emph{miscellaneous}.  This classification is

790: represented using kind theory's inheritance operators.

791: 

792: % (+ 8 3 5 1 3 3 2 4 2 4)

793: 

794: Many of these semantic properties are used solely for documentation

795: purposes.  The \texttt{title} property documents the title of the project

796: with which a file is associated; the \texttt{description} property provides

797: a brief summary of the contents of a file.  We call these \emph{informal}

798: semantic properties.

799: 

800: Another set of properties are used for specifying non-program\-matic

801: semantics.  By ``non-programmatic'' we mean that the properties have

802: semantics, but they are not, or cannot, be expressed in program code.  For

803: example, labeling a construct with a \texttt{copyright} or \texttt{license}

804: property specifies some legal semantics.  Tagging a method with a

805: \texttt{bug} property specifies that the method has some erroneous behavior

806: that is described in detail in an associated bug report.  We call these

807: properties \emph{semi-formal} because they have a semantics, but outside of

808: the domain of software.

809: 

810: Finally, the balance of the properties specify structure that is

811: programmatically testable, checkable, or verifiable.  Basic examples of

812: such properties are \texttt{require} and \texttt{ensure} tags for

813: preconditions and postconditions, \texttt{modifies} tags for side-effect

814: semantics, and the \texttt{concurrency} and \texttt{generate} tags for

815: concurrency semantics.  These properties are called \emph{formal} because

816: they can be realized by a formal semantics.

817: 

818: The KindSoftware coding standard~\cite{KS-Code_Standard01} summarizes our

819: current set of semantic properties.  Each property has a syntax, a correct

820: usage domain, and a natural language summary.  The formalization of

821: semantic properties is found in Kiniry's dissertation~\cite{Kiniry02-PhD}.

822: 

823: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

824: \subsection{Context}

825: \label{sec:context}

826: 

827: Each property has a legal scope of use, called its \emph{context}.

828: Contexts are defined in a coarse, language-independent fashion using

829: inclusion operators in kind theory.  Contexts are comprised of

830: \emph{files}, \emph{modules}, \emph{features}, and \emph{variables}.

831: 

832: \emph{Files} are exactly that: data files in which program code resides.

833: The scope of a file encompasses everything contained in that file.

834: 

835: A \emph{module} is some large-scale program unit.  Modules are typically

836: realized by an explicit module- or class-like structure.  Examples of

837: modules are classes in object-oriented systems, modules in languages of the

838: Modula and ML families, packages in the Ada lineage, etc.  Other words and

839: structures typically bound to modules include units, protocols, interfaces,

840: etc.

841: 

842: \emph{Features} are the entry point for computation.  Features are often

843: named, have parameters, and return values.  Functions and procedures in

844: structured languages are features, as are methods in object-oriented

845: languages, and functions in functional systems.

846: 

847: Finally, \emph{variables} are program variables, attributes, constants,

848: enumerations, etc.  Because few languages enforce any access principles for

849: variables, variables can vary in semantics considerably.

850: 

851: Each property listed in the appendix has a legal context.  The context

852: \emph{All} means that the property can be used at the file, module,

853: feature, or variable level.  Additional contexts can be defined, extending

854: the semantics of contexts for new programming language constructs that need

855: structured documentation with properties.

856: 

857: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

858: \subsection{Visibility}

859: \label{sec:visibility}

860: 

861: In languages that have a notion of \emph{visibility}, a property's

862: visibility is equivalent to the visibility of the context in which it is

863: used, augmented by domain-specific visibility options expressed in kind

864: theory.

865: 

866: Typical basic notions of visibility include \emph{public}, \emph{private},

867: \emph{children} (for systems with inheritance), and \emph{module} (e.g.,

868: Java's \emph{package} visibility).  More complex notions of visibility are

869: exhibited by C++'s notion of \emph{friend} and Eiffel's class-based feature

870: scoping.

871: 

872: Explicit visibilities for semantic properties are used to refine the notion

873: of specification visibility for organizational, social, and formal reasons.

874: 

875: For example, a subgroup of a large development team might choose to expose

876: some documentation for, and specification of, their work only to specific

877: other groups for testing, political, or legal reasons.

878: 

879: On the social front, new members of a team might not have yet learned

880: specific tools or formalisms used in semantic properties, so using

881: visibility to hide those properties will help avoid information overload.

882: 

883: Lastly, some formal specification, especially when viewed in conjunction

884: with standard test strategies (e.g., whitebox, greybox, blackbox, unit

885: testing, scenario-based testing), has distinct levels of visibility.  For

886: example, testing the postcondition of a private feature is only reasonable

887: and permissible if the testing agent is responsible for that private

888: feature.

889: 

890: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

891: \subsection{Inheritance}

892: \label{sec:inheritance}

893: 

894: Semantic properties also have a well-defined notion of \emph{property

895:   inheritance}.  Once again, we do not want to force new and complicated

896: extra-language semantics on the software engineer.  Therefore, property

897: inheritance semantics match those of the source language in which the

898: properties are used.  Our earlier discussion of basic comments for Java

899: methods (a feature property context) is an example of such property

900: inheritance.

901: 

902: These kinds of inheritance come in two basic forms: \emph{replacement} and

903: \emph{augmentation}.

904: 

905: The \emph{replacement} form of inheritance means that the parent property

906: is completely replaced by the child property.  An example of such semantics

907: are feature overriding in Java and the associated documentation semantics

908: thereof.

909: 

910: \emph{Augmentation}, on the other hand, means that the child's properties

911: are actually a \emph{composition} of all its parents' properties.  These

912: kinds of composition come in several forms.  The most familiar is the

913: standard substitution principle-based type semantics~\cite{LiskovWing93} in

914: many object-oriented systems, and the Hoare logic/Dijkstra calculus-based

915: semantics of contract refinement~\cite{Meyer92b}.

916: 

917: We can express these formal notions using kind theory because it is

918: embedded in a complete logical framework.  For example, we can

919: automatically reason about the legitimacy of specification refinement much

920: like Findler and Felleisen discuss in~\cite{FindlerFelleisen01}.

921: 

922: %%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

923: %\subsection{Conventions and Code Standards}

924: 

925: %Rigorous use of semantic properties makes for more complete and correct

926: %documentation and program code.  The first stage of such use is the

927: %explicit adoption of a coding standard that incorporates semantic

928: %properties.

929: 

930: %We have defined a set of conventions used in all of our projects and all of

931: %the courses that we teach.  The following is a partial distillation of our

932: %own coding standard~\cite{KS-Code_Standard01}.

933: 

934: %\subsubsection{File Comment}

935: 

936: %Every file has a file comment containing at least the following

937: %information:

938: %\begin{enumerate}

939: %\item The title of the project with which this module is associated using

940: %  the \texttt{title} property.

941: %\item A short description of the file's contents using the

942: %  \texttt{description} property.

943: %\item Any copyright information relevant to the project using the

944: %  \texttt{copyright} property.

945: %\item The license(s) under which the file is protected using the

946: %  \texttt{license} property.

947: %\item The primary authors of the file using the \texttt{author} property.

948: %\item Using a \texttt{version} property, document the RCS

949: %  \emph{\$Revision\$} tag.

950: %\end{enumerate}

951: 

952: %\subsubsection{Module Comment}

953: 

954: %A module comment describes the purpose of the module, guaranteed

955: %invariants, usage instructions, and/or usage examples. The beginning of the

956: %comment contains a description of the module in exactly one sentence using

957: %the \texttt{bon} property.  That summary is used by our EBON tool,

958: %described later.  Also included in the class comment are any reminders or

959: %disclaimers about required or desired improvements.

960: 

961: %Each class comment block must include exactly one \texttt{version} property

962: %and at least one \texttt{author} property. The \texttt{author} properties

963: %often list everyone who has written more than a few lines of the class.

964: %Each \texttt{author} property should list exactly one author. The

965: %\texttt{version} property's version is a project-specific string (e.g.,

966: %``1.0b5c7'') followed by a RCS \emph{\$Date\$} tag.

967: 

968: %\subsubsection{Feature Comment}

969: 

970: %Use language and local documentation conventions to describe nature,

971: %purpose, specification, effects, algorithmic notes, usage instructions,

972: %reminders, etc. for each any every feature. The beginning of a method

973: %comment should be a summary of the method in exactly one sentence using the

974: %\texttt{bon} property.

975: 

976: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

977: \subsection{Tool Support}

978: \label{sec:tool-support}

979: 

980: We have used these semantic properties for the last five years.  We have

981: found that, while an explicit adopted coding standard, positive feedback

982: via tools and peers, and course grade and monetary rewards goes a long way

983: toward raising the bar for documentation and specification quality, these

984: social aspects are simply not enough.  Process does help, regular code

985: reviews and pair programming in particular, but tool support is critical to

986: maintaining quality specification coverage, completeness, and consistency.

987: 

988: Templates were the first step taken.  We have used raw documentation and

989: code templates in programming environments ranging from \emph{vi} to

990: \emph{emacs} to \emph{jEdit}.  But templates only help prime the process,

991: they do not help maintain the content.

992: 

993: Code and comment completion also helps.  Completion is the ability of an

994: environment to use partial input to derive a typically more lengthy full

995: input.  We have experimented with augmented versions of completion in

996: \emph{emacs}, for example.

997: 

998: Likewise, documentation lint checkers, particularly those embedded in

999: development environments and documentation generators are also useful.  We

1000: view source text highlighting, as in \emph{font-lock} mode in emacs, as an

1001: extremely weak form of lint-checking.  The error reports issued by Javadoc

1002: and its siblings are a stronger form of lint-checking and are quite useful

1003: for documentation coverage analysis, especially when a part of the regular

1004: build process.  Finally, scripts integrated into a revision control system

1005: provide a ``quality firewall'' to a source code repository in much the same

1006: fashion.

1007: 

1008: We believe that more can and should be done.  Our approach is to build and

1009: use what we call \emph{Knowledgeable Development Environments} (KDEs).

1010: These development environments use knowledge representation and formal

1011: reasoning behind the scenes to help the user work smarter and not harder.

1012: 

1013: We have started work on such environment.  By extending powerful emacs

1014: modes and tools that are part of our initial development environment (e.g.,

1015: XEmacs coupled with the object-oriented browser, hyperbole, JDE, semantic,

1016: and speedbar) with a kind system, we hope to raise the bar on development

1017: environments.

1018: 

1019: %---------------------------------------------------------------------

1020: \subsubsection{Current Work on KDEs}

1021: \label{sec:current-work-kdes}

1022: 

1023: The first two features that we plan to implement are \emph{documentation

1024:   inheritance} and \emph{perspective}.

1025: 

1026: Eiffel development environments contain tools that provide what are called

1027: the \emph{flat}, \emph{short}, and \emph{contract} views of a class.  Flat

1028: forms show the flattened version of a class---all inherited features are

1029: flattened into a single viewpoint.  The short form eliminates the

1030: implementation of all methods so that the developer can focus on a class's

1031: interface.  The contract form is like the short form except the contracts

1032: of the class (feature preconditions and postcondition, and class

1033: invariants) are shown.  These forms can be combined, thus \emph{flat short}

1034: or \emph{flat contract} forms have the obvious meanings.

1035: 

1036: \emph{Knowledgeable documentation inheritance} is an extended version of

1037: such views.  Rather than manually program the semantics of the

1038: ``flattening'' operation, our formal specification in kind theory

1039: automatically interprets the appropriate instances into a new form for

1040: rendering within the knowledgeable development environment.  And because

1041: such interpretations are often fully reversible, the flattened forms can be

1042: edited and the changes will properly ``percolate'' to their original source

1043: locations.

1044: 

1045: \emph{Perspectives} enable the user to specify which role(s) she is in

1046: while interacting with the kind-enabled system.  Since kind theory is

1047: autoepistemic, the specification of a role (represented by an \emph{agent}

1048: within the theory) permits automatic ``filtering'' of information according

1049: to, for example, visibility rules as discussed in

1050: Section~\ref{sec:visibility}.  This user-centric filtering of information,

1051: much like narrowing modes within Emacs, helps the user focus on the problem

1052: at hand, ignoring all information that she either is not interested in,

1053: concerned with, or should not see.

1054: 

1055: These are only two of our ideas for how to expose the user-centric aspects

1056: of kind theory via development environments, incorporating the use of

1057: semantic properties throughout.

1058: 

1059: %=====================================================================

1060: \section{Embedding Semantic Properties}

1061: \label{sec:embedd-semant-prop}

1062: 

1063: When a semantic property is bound to a particular instance, for example, an

1064: \texttt{@author} tag is used in some Java source code, what does this

1065: formally mean beyond questions of structural conformance?  How do these

1066: semantic properties help guide the development process and exercise the

1067: system during testing?  How do new tools take advantage of these

1068: properties?

1069: 

1070: First, we have to \emph{embed} the semantic properties into the language in

1071: which we are working.  Second, we need to define domain-specific semantics

1072: using kind interpretations.  Lastly, we use kind theory's belief truth

1073: structures to guide program development.

1074: 

1075: We will first look at syntactic embedding for two programming and one

1076: specification language.  In the latter parts of this next section we will

1077: address the other two points.

1078: 

1079: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1080: \subsection{Programming Languages}

1081: \label{sec:progr-lang}

1082: 

1083: We have used semantic extensions in two programming languages: Java and

1084: Eiffel.

1085: 

1086: %---------------------------------------------------------------------

1087: \subsubsection{Java}

1088: \label{sec:java}

1089: 

1090: Semantic properties are embedded in Java code using Javadoc-style comments.

1091: This makes for a simple, parseable syntax, and the kind composition of

1092: semantic properties to constructs is simply realized by textual

1093: concatenation.

1094: 

1095: Here is an example of such use, taken directly from one of our projects

1096: that uses semantic properties~\cite{KiniryIDebug98}.

1097: 

1098: \scriptsize

1099: \begin{verbatim}

1100: /**

1101:  * Returns a boolean indicating whether any debugging 

1102:  * facilities are turned off for a particular thread.

1103:  *

1104:  * @concurrency GUARDED

1105:  * @require (thread != null) Parameters must be valid.

1106:  * @modify QUERY

1107:  * @param thread we are checking the debugging condition 

1108:  * of this thread.

1109:  * @return a boolean indicating whether any debugging 

1110:  * facilities are turned off for the specified thread.

1111:  * @review kiniry Are the isOff() methods necessary at all?

1112:  **/

1113:      

1114:  public synchronized boolean isOff(Thread thread)

1115:  {

1116:    return (!isOn(thread));

1117:  }

1118: \end{verbatim}

1119: \normalsize

1120: 

1121: Existing tools already use these properties for translating specifications,

1122: primarily in the form of contracts, into run-time test code.  Reto Kramer's

1123: iContract~\cite{Kramer98}, the University of Oldenburg's Semantic Group's

1124: Jass tool, Findler and Felliason's contract soundness checking

1125: tool~\cite{FindlerFelleisen01}, and Kiniry and Cheong's

1126: JPP~\cite{KiniryCheong98} are three such tools.

1127: 

1128: %---------------------------------------------------------------------

1129: \subsubsection{Eiffel}

1130: \label{sec:eiffel}

1131: 

1132: In Eiffel, as mentioned earlier, we use indexing clauses as well as

1133: regularly structured comments to denote semantic properties.  Using

1134: comments as well as indexing clauses is necessary because the syntax of

1135: Eiffel dictates that indexing clauses only appear at the top of a source

1136: file.  The syntax of comments that use semantic properties is identical to

1137: that of indexing clauses, thus the same parser code can be used in both

1138: instances.  An example of such use is as follows, directly from one of our

1139: Eiffel-based projects that uses semantic properties~\cite{EBON01}.

1140: 

1141: \scriptsize

1142: \begin{verbatim}

1143: indexing

1144:    description: "The Extended BON scanner."

1145:    project:     "The Extended BON Tool Suite"

1146:    author:      "Joseph R. Kiniry <kiniry@acm.org>"

1147:    copyright:   "Copyright (C) 2001 Joseph R. Kiniry"

1148:    version:     "$Revision: 1.10 $"

1149:    license:     "Eiffel Forum Freeware License v1"

1150: \end{verbatim}

1151: \normalsize

1152: 

1153: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1154: \subsection{Specification Languages}

1155: \label{sec:spec-lang}

1156: 

1157: We have also used semantic properties to extend the BON specification

1158: language.

1159: 

1160: %---------------------------------------------------------------------

1161: \subsubsection{BON}

1162: \label{sec:bon}

1163: 

1164: BON stands for the \emph{Business Object Notation}.  BON is described in

1165: whole in Walden and Nerson's \emph{Seamless Object-Oriented Software

1166:   Architecture}~\cite{WaldenNerson94}, extended from an earlier paper by

1167: Nerson~\cite{Nerson92}.

1168: 

1169: \paragraph{Primary Aspects}

1170: BON is an unusual specification language in that it is \emph{seamless},

1171: \emph{reversible}, and focuses on \emph{contracting}.  BON also has both a

1172: textual and a graphical form.

1173: 

1174: BON is \emph{seamless} because it is designed to be used during all phases

1175: of program development.  Multiple refinement levels (high-level design with

1176: charts, detailed design with types, and dynamism with scenarios and

1177: events), coupled with explicit refinement relationships between those

1178: levels, means that BON can be used all the way from domain analysis to unit

1179: and system testing and code maintenance.

1180: 

1181: \emph{Reversibility} summarizes the weak but invertible nature of BON's

1182: semantics.  By virtue of its design, every construct described in BON is

1183: fully realizable in program code.  One can specify system structure, types,

1184: contracts, events, scenarios, and more.  Each of these constructs can not

1185: only be interpreted into program code, but program code can be interpreted

1186: into BON.  As far as we are aware, this makes BON unique insofar as, with

1187: proper tool support, a system specification need not become out-of-date if

1188: it is written in BON.

1189: 

1190: Finally, BON focuses on software \emph{contracts} as a primary means of

1191: expressing system semantics.  These contracts have exactly the same

1192: semantics as discussed earlier with regards to object-oriented models,

1193: because BON is an object-oriented specification language.

1194: 

1195: BON's semantics were originally specified informally using

1196: Eiffel~\cite{Meyer88, WaldenNerson94}.  Paige and Ostroff recently provided

1197: an analysis of BON with an eye toward a refinement-centric formal

1198: semantics~\cite{PaigeOstroff01a, PaigeOstroff01b}.

1199: 

1200: \paragraph{BON Technologies}

1201: BON has been, and is being, used within several commercial and Open Source

1202: tools: Interactive Software Engineering's EiffelCase and

1203: \myhref{http://www.eiffel.com/products/studio51/}{EiffelStudio} tools;

1204: Ehrke's BonBon CASE tool; Steve Thompson and Roy Phillips's BONBAZ/Envision

1205: project; Kaminskaya's BON static diagram tool~\cite{Kaminskaya01}; Paige,

1206: Lancaric, and Ostroff's BON CASE tool; and Kiniry's EBON tool

1207: suite~\cite{EBON01}.

1208: 

1209: The last three are particularly exciting projects because they are

1210: currently active and have wide applicability.  Kaminskaya's and Lancaric's

1211: tools generate textual BON, JML, Eiffel, and Java source code from a

1212: graphical BON specification.

1213: 

1214: %---------------------------------------------------------------------

1215: \subsubsection{Extended BON}

1216: \label{sec:extended-bon}

1217: 

1218: Kiniry's EBON tool suite has a different aim.  Its secondary purpose is

1219: similar to other previously mentioned tools, namely the generation of

1220: documentation from BON specifications.  But its primary use is \emph{design

1221:   model checking} for Eiffel and Java code.

1222: 

1223: BON is extended with our set of semantic properties by (a) extending the

1224: BON language (adding new keywords and expressions), (b) using structured

1225: comments, and (c) using indexing clauses like those in Eiffel.  More

1226: information on these specific extensions is available at the EBON web

1227: site~\cite{EBON01}.

1228: 

1229: \paragraph{Domain-Specific Semantics}

1230: Translations from BON to a source language and vice-versa are to be

1231: represented by kind theory interpretations.  This means that changes to

1232: either side of the translation can not only be translated, but can be

1233: checked for validity according to its (dual) model.  This

1234: specification-code conformance (validity) checking is what we call

1235: \emph{design model checking}.  We use this terminology because the

1236: specification is the theory and the program code is the model, when viewed

1237: from the logical perspective.

1238: 

1239: A change in the source code that is part of a EBON interpretation image

1240: will automatically trigger a corresponding change in the EBON

1241: specification.  Likewise, any change in the EBON specification will

1242: automatically trigger a corresponding change in the source code.

1243: 

1244: Some of these translations entail more than just a transfer of information

1245: from a specification to a comment in the source code.  For example, an

1246: \texttt{invariant} semantic tag is interpreted not only as documentation,

1247: but also as run-time test code.  We do not have the space in this paper to

1248: detail this interpretation.  It follows the same lines as related tools

1249: that support contract-based assertions in Java and Eiffel mentioned

1250: elsewhere in this paper.

1251: 

1252: \paragraph{Belief-Driven Development}

1253: Some BON extensions are \emph{non-reversible} because they represent system

1254: aspects that are either very difficult or impossible to derive.  For

1255: example, the \texttt{time\--complexity} semantic property specifies the

1256: computational complexity of a feature.  It is (rarely) possible to extract

1257: such information from an algorithm with automated tools.  But the fact is,

1258: the algorithm author often knows her algorithm's complexity.  Thus, stating

1259: the complexity as part of the algorithm specification with a semantic

1260: property is easy and straightforward task.

1261: 

1262: Now the question arises: How do we know such specifications that are not

1263: automatically checkable remain valid?  This is where the earlier-mentioned

1264: belief truth structures of kind theory come into play.  

1265: 

1266: When the programmer writes the original \texttt{time\--complexity} semantic

1267: property for a feature, she is stating a \emph{belief} about that feature.

1268: Beliefs in kind theory are autoepistemic (the representation of the

1269: programmer is part of the logical sentence encoding the belief), have an

1270: associated ``strength'' or ``surety'' metric (recall

1271: Section~\ref{sec:brief-overview-kind}), and include a set of

1272: \emph{evidence} supporting the belief.  

1273: 

1274: We use a number of techniques to ensure that old or out-of-date beliefs are

1275: rechecked.  With regards to this example, we define a \emph{continued

1276:   validity condition} as part of the evidence, which is machine checkable.

1277: Currently, if the program code or documentation to which the complexity

1278: metric belief is bound radically changes in size, or if the feature has a

1279: change in type, author, or other potentially complexity-impacting

1280: specification (e.g., concurrency, space-complexity, etc.), then the

1281: validity condition is tripped and the developer is challenged to re-check

1282: and validate the belief, restarting the process.

1283: 

1284: %=====================================================================

1285: \section{Experiences}

1286: \label{sec:experiences}

1287: 

1288: We have used semantic properties within our research group, in the

1289: classroom, and in two corporate settings.

1290: 

1291: The Compositional Computing Group at Caltech has used semantic properties

1292: in our complex, distributed and concurrent architectures, written in Java

1293: and Eiffel, over the past five years.  We have witnessed their utility by

1294: first-hand experience primarily during the introduction of our complex

1295: technologies to new students and collaborators is particularly facilitated

1296: by semantic properties.

1297: 

1298: Students grumble at first when they are told that their comments now have a

1299: precise syntax and a semantics.  The students initially think of this as

1300: being ``just more work'' on their part---yet another reason to hand in a

1301: late assignment.  But, as the term goes by, the students incorporate the

1302: precise documentation with semantic properties and related tools into their

1303: development process.  After a few weeks of indoctrination, they not only

1304: stop complaining, but start praising the process and tools.  We generally

1305: see higher quality systems and the students report spending \emph{less}

1306: time on their homework than when they started the course.  They have

1307: learned how to work \emph{smarter}, not \emph{harder}.

1308: 

1309: These languages, process, and tools were also used in a corporate setting

1310: to develop a enormously complex, distributed, concurrent architecture.

1311: When showing the system to potential funders and collaborators, being able

1312: to present the system architecture and code with this level of

1313: specification and documentation invariably increased our value proposition.

1314: Uniformly, investors were not only shocked that a startup would actually

1315: \emph{design} their system, but to think that we used lightweight formal

1316: methods to design, build, test, and document the system was absolutely

1317: unheard of.

1318: 

1319: We have incorporated feedback from these three domains into our work.  Our

1320: set of semantic properties is still evolving, albeit at a rapidly

1321: decreasing rate.  Our tools see refinement for incorporation into new

1322: development processes, better error handling, and more complete and correct

1323: functionality.  This user feedback is essential to understanding how these

1324: technologies and theory can be exposed in academic and industrial settings.

1325: 

1326: %=====================================================================

1327: % Conclusion assessing the results of the work described and its

1328: % limitations.

1329: %=====================================================================

1330: \section{Conclusion}

1331: \label{sec:conclusion}

1332: 

1333: Documentation reuse is most often discussed in the literate

1334: programming~\cite{ChildsSametinger96} and hypertext

1335: domains~\cite{FischerMcCallMorch89}.  Little research exists for

1336: formalizing the semantics of semi-structured documentation.  Some work in

1337: formal concept analysis and related formalisms~\cite{SimosAnthony98,

1338:   Wille92} has started down this path, but with extremely loose semantics

1339: and little to no tool support.

1340: 

1341: Recent work by Wendorff~\cite{Wendorff99, Wendorff01} bears resemblance to

1342: this work both in its nature (that of concept formation and resolution) and

1343: theoretic infrastructure (that of category theory).  Our work is

1344: differentiated by its broader scope, its more expressive formalism, and its

1345: realization in tools.  Additionally, the user-centric nature of kind theory

1346: (not discussed in this article) makes for exposing the formalism to the

1347: typical software engineer a straightforward practice.

1348: 

1349: Our next steps are on two fronts.  First, we are interested in embedding

1350: our semantic properties in the Java-centric specification language JML.

1351: Second, we are continuing to develop new tools and technologies to realize

1352: knowledgeable development environments that use kind theory as a formal

1353: foundation.

1354: 

1355: %---------------------------------------------------------------------

1356: \subsection{JML}

1357: \label{sec:jml}

1358: 

1359: JML is the Java Modeling Language~\cite{LeavensBakerRuby99}.  JML is a

1360: Java- and model-centric language in the same tradition as Larch and VDM.

1361: JML is used to specify detailed semantic aspects of Java code and some tool

1362: support exists for type-checking and translating these specifications into

1363: documentation and run-time test code~\cite{Bhorkar00, Ganapathy99,

1364:   Raghavan00}.  The formal semantics of JML have been partially specified

1365: via a logic as part of the LOOP project~\cite{JacobsPoll00}.

1366: 

1367: Extending JML with semantic properties would follow the same course that we

1368: have used for BON.  Because we already have integrated semantic properties

1369: with Java, and given the existing tool support for JML, we should be able

1370: to realize inter-domain interpretations that preserve a vast amount of

1371: information about JML-specified Java systems using kind theory.

1372: 

1373: %---------------------------------------------------------------------

1374: \subsection{Social Implications}

1375: \label{sec:social-implications}

1376: 

1377: We expect that knowledgeable development environments will have social

1378: implications for software development.

1379: 

1380: First, this challenging, interactive style imposed by knowledgeable

1381: development environments is not typical---we have to make sure that we are

1382: not introducing some kind of formal methods ``paper clip''.  Thus, the

1383: environment needs to ``tune'' itself to the interactive style and

1384: development process of the user.  We look forward to theoretically

1385: representing such styles in kind theory so that tuning is simply part of

1386: the logical context.

1387: 

1388: Second, in our extensive experience in the research lab, classroom, and

1389: corporate office, we have witnessed the fact that most developers are very

1390: uncomfortable \emph{starting from scratch}, especially with regards to

1391: system documentation and informal and formal specifications.  If some

1392: existing documentation or specification exists, developers are much more

1393: likely to continue in that trend because they feel that they are

1394: \emph{contributing} rather than \emph{creating}.  

1395: 

1396: Because the EBON tool suite will automatically generate a base

1397: specification from program code, and because the specification-code

1398: validity conformance is automatically maintained, we have a primer as well

1399: as a positive feedback cycle for lightweight specification with semantic

1400: properties.  Only time and experience will tell whether this is a

1401: sufficient fire to light the correct software fuse.

1402: 

1403: %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1404: \subsection{Knowledgeable Environments}

1405: \label{sec:knowl-envir}

1406: 

1407: As mentioned previously, our work on KDEs continues.  

1408: 

1409: We wish to augment our already powerful development environment in two

1410: ways.  Our first step entails integrating an interactive front-end like

1411: XEmacs with our kind system realized in Maude.  The availability of

1412: Emacs-centric tools for proof system like the excellent

1413: \myhref{http://zermelo.dcs.ed.ac.uk/$\sim$proofgen/}{Proof General} make

1414: this a relatively straightforward exercise.  The most time-consuming aspect

1415: is writing interpretation engines that translate annotated source code to

1416: and from a kind representation format.  Several such tools are being

1417: prototyped now~\cite{EBON01, KiniryCheong98}.

1418: 

1419: We also plan on integrating these environments with our reusable knowledge

1420: repository known as the Jiki~\cite{Jiki98}.  The Jiki is a read/write web

1421: architecture realized as a distributed component-based Java Wiki.  All

1422: documents stored in the Jiki are represented as instances of kind.

1423: Manipulating Jiki assets, including adding or deleting information or

1424: searching for reusable assets, is realized through a forms-based web

1425: interface as well as through a Java component-based API.

1426: 

1427: %=====================================================================

1428: \section{Acknowledgments}

1429: 

1430: This work was supported under ONR grant JJH1.MURI-1-CORNELL.MURI (via

1431: Cornell University) ``Digital Libraries: Building Interactive Digital

1432: Libraries of Formal Algorithmic Knowledge'' and AFOSR grant

1433: JCD.\-61404-1-AFOSR.\-614040 ``High-Confidence Reconfigurable Distributed

1434: Control''.

1435: 

1436: %======================================================================

1437: 

1438: \bibliographystyle{plain}

1439: %\bibliography{bibliography/abbrev,bibliography/ads,bibliography/category,bibliography/complexity,bibliography/conferences,bibliography/hypertext,bibliography/icsr,bibliography/journals,bibliography/knowledge,bibliography/languages,bibliography/linguistics,bibliography/meta,bibliography/metrics,bibliography/misc,bibliography/modeling,bibliography/modeltheory,bibliography/reuse,bibliography/rewriting,bibliography/softeng,bibliography/specification,bibliography/ssr,bibliography/technology,bibliography/theory,bibliography/upcoming,bibliography/upcoming_conferences,bibliography/web,bibliography/workshops}

1440: 

1441: %======================================================================

1442: 

1443: \begin{thebibliography}{10}

1444: 

1445: \bibitem{Bench-CaponMalcolm99}

1446: T.~Bench-Capon and G.~Malcolm.

1447: \newblock {\em Formalising Ontologies and Their Relations}, volume 1677 of {\em

1448:   Lecture Notes in Computer Science}, pages 250--259.

1449: \newblock Springer--Verlag, 1999.

1450: 

1451: \bibitem{Bhorkar00}

1452: Abhay Bhorkar.

1453: \newblock A run-time assertion checker for {Java} using {JML}.

1454: \newblock Technical Report 00-08, Department of Computer Science, Iowa State

1455:   University, May 2000.

1456: 

1457: \bibitem{ChildsSametinger96}

1458: Bart Childs and Johannes Sametinger.

1459: \newblock Literate programming and documentation reuse.

1460: \newblock In {\em Proceedings of the Fourth International Conference on

1461:   Software Reuse}, pages 205--214, 1996.

1462: 

1463: \bibitem{ClavelDuranEtal99-Metatool}

1464: Manuel Clavel, Francisco Dur{\'a}n, Steven Eker, Jos{\'e} Meseguer, and

1465:   Mark-Oliver Stehr.

1466: \newblock Maude as a formal meta-tool.

1467: \newblock In {\em Proceedings of the World Congress on Formal Methods in the

1468:   Development of Computing Systems}, 1999.

1469: 

1470: \bibitem{FindlerFelleisen01}

1471: R.~Findler and M.~Felleisen.

1472: \newblock Contract soundness for object-oriented languages.

1473: \newblock In {\em Proceedings of Sixteenth International Conference

1474:   Object-Oriented Programming, Systems, Languages, and Applications}, 2001.

1475: 

1476: \bibitem{FischerMcCallMorch89}

1477: G.~Fischer, R.~McCall, and A.~Morch.

1478: \newblock {JANUS}: Integrating hypertext with a knowledge-based design

1479:   environment.

1480: \newblock {\em SIGCHI Bulletin}, pages 105--117, 1989.

1481: 

1482: \bibitem{Ganapathy99}

1483: Anand Ganapathy.

1484: \newblock Design and implementation of a {JML} type checker.

1485: \newblock Master's thesis, Iowa State University, 1999.

1486: 

1487: \bibitem{Gruber00}

1488: T.~Gruber.

1489: \newblock Towards principles for the design of ontologies used for knowledge

1490:   sharing.

1491: \newblock In N.~Guarino and R.~Poli, editors, {\em Formal Ontology in

1492:   Conceptual Analysis and Knowledge Representation}. Kluwer Academic

1493:   Publishing, 2000.

1494: \newblock In prepartation.

1495: 

1496: \bibitem{HerzigGogolla92}

1497: R.~Herzig and M.~Gogolla.

1498: \newblock Transforming conceptual data models into an object model.

1499: \newblock {\em Lecture Notes in Computer Science}, 645:280--298, 1992.

1500: 

1501: \bibitem{JacobsPoll00}

1502: Bart Jacobs and Erik Poll.

1503: \newblock A logic for the {Java} modeling language {JML}.

1504: \newblock Technical Report CSI-R0018, Computing Science Institute, University

1505:   of Nijmegen, November 2000.

1506: 

1507: \bibitem{Kaminskaya01}

1508: Liliya Kaminskaya.

1509: \newblock Combining tools for object-oriented software development: An

1510:   integration of {BON} and {JML}.

1511: \newblock Master's thesis, Department of Computer Science, York University,

1512:   2001.

1513: 

1514: \bibitem{KiniryIDebug98}

1515: Joseph~R. Kiniry.

1516: \newblock {IDebug}: An advanced debugging framework for {Java}.

1517: \newblock Technical Report CS-TR-98-16, Department of Computer

1518:   Science,California Institute of Technology, November 1998.

1519: 

1520: \bibitem{Jiki98}

1521: Joseph~R. Kiniry.

1522: \newblock The {Jiki}: A distributed component-based {Java Wiki}.

1523: \newblock Available via \href{http://www.jiki.org/} {http://www.jiki.org/},

1524:   1998.

1525: 

1526: \bibitem{EBON01}

1527: Joseph~R. Kiniry.

1528: \newblock The {Extended BON} tool suite.

1529: \newblock \href{http://ebon.sourceforge.net/} {http://ebon.sourceforge.net/},

1530:   2001.

1531: 

1532: \bibitem{Kiniry02-PhD}

1533: Joseph~R. Kiniry.

1534: \newblock {\em Formalizing Open, Collaborative Reuse with Kind Theory}.

1535: \newblock PhD thesis, California Institute of Technology, 2002.

1536: 

1537: \bibitem{KiniryCheong98}

1538: Joseph~R. Kiniry and Elaine Cheong.

1539: \newblock {JPP}: A {Java} pre-processor.

1540: \newblock Technical Report CS-TR-98-15, Department of Computer

1541:   Science,California Institute of Technology, November 1998.

1542: 

1543: \bibitem{Knuth92}

1544: Donald~E. Knuth.

1545: \newblock {\em Literate Programming}.

1546: \newblock Number~27 in {CSLI} Lecture Notes. Center for the Study of Language

1547:   and Information, 1992.

1548: 

1549: \bibitem{KnuthLevy93}

1550: Donald~E. Knuth and Silvio Levy.

1551: \newblock {\em The {CWEB} System of Structured Documentation}.

1552: \newblock Addison-Wesley Publishing Company, third edition, 2001.

1553: 

1554: \bibitem{Kramer98}

1555: Reto Kramer.

1556: \newblock {iContract}--­the {Java} design by contract tool.

1557: \newblock In {\em Proceedings of the Twenty-Fourth Conference on the Technology

1558:   of Object-Oriented Languages ({TOOLS} 24)}, volume~26 of {\em TOOLS

1559:   Conference Series}. IEEE Computer Society, 1998.

1560: 

1561: \bibitem{LeavensBakerRuby99}

1562: Gary~T. Leavens, Albert~L. Baker, and Clyde Ruby.

1563: \newblock {\em Behavioral Specifications of Business and Systems}, chapter

1564:   {JML}: A Notation for Detailed Design, pages 175--188.

1565: \newblock Kluwer Academic Publishing, 1999.

1566: 

1567: \bibitem{LiskovWing93}

1568: Barbara Liskov and Jeannette~M. Wing.

1569: \newblock Specifications and their use in defining subtypes.

1570: \newblock In {\em ACM Conference on Object-Oriented Programming Systems,

1571:   Languages, and Applications}, pages 16--28. ACM SIGPLAN: Programming

1572:   Languages, ACM Press and Addison-Wesley Publishing Company, 1993.

1573: 

1574: \bibitem{Meyer88}

1575: Bertrand Meyer.

1576: \newblock {\em Object-Oriented Software Construction}.

1577: \newblock Prentice-Hall, Inc., second edition, 1988.

1578: 

1579: \bibitem{Meyer90-ETL}

1580: Bertrand Meyer.

1581: \newblock {\em Eiffel the Language}.

1582: \newblock Prentice-Hall, Inc., third edition, 1990.

1583: 

1584: \bibitem{Meyer92b}

1585: Bertrand Meyer.

1586: \newblock Applying design by contract.

1587: \newblock {\em IEEE Computer}, October 1992.

1588: 

1589: \bibitem{Nerson92}

1590: Jean-Marc Nerson.

1591: \newblock Applying object-oriented analysis and design.

1592: \newblock {\em Communications of the ACM}, 35(9):63--74, September 1992.

1593: 

1594: \bibitem{PaigeOstroff01a}

1595: Richard Paige and Jonathan~S. Ostroff.

1596: \newblock {ERC} - {An} object-oriented refinement calculus for {Eiffel}.

1597: \newblock Technical Report CS-2001-05, Department of Computer Science, York

1598:   University, August 2001.

1599: 

1600: \bibitem{PaigeOstroff01b}

1601: Richard~F. Paige and Jonathan Ostroff.

1602: \newblock Metamodelling and conformance checking with {PVS}.

1603: \newblock In {\em Proceedings of Fundamental Aspects of Software Engineering},

1604:   volume 2029 of {\em Lecture Notes in Computer Science}. Springer--Verlag,

1605:   April 2001.

1606: \newblock Also available via

1607:   \href{http://www.cs.yorku.ca/techreports/2000/CS-2000-03.html}{http://www.cs%

1608: .yorku.ca/techreports/2000/CS-2000-03.html}.

1609: 

1610: \bibitem{Raghavan00}

1611: Arun~D. Raghavan.

1612: \newblock Design of a {JML} documentation generator.

1613: \newblock Technical Report 00-12, Department of Computer Science, Iowa State

1614:   University, March 2000.

1615: 

1616: \bibitem{SimosAnthony98}

1617: M.~Simos and J.~Anthony.

1618: \newblock Weaving the model web: A multi-modeling approach to concepts and

1619:   features in domain engineering.

1620: \newblock In {\em Proceedings of the Fifth International Conference on Software

1621:   Reuse}, Victoria, BC, Canada, 1998.

1622: 

1623: \bibitem{VandervetMars98}

1624: {P.E.} van~der Vet and {N.J.I.} Mars.

1625: \newblock Bottom-up construction of ontologies.

1626: \newblock {\em IEEE Transactions on Knowledge and Data Engineering},

1627:   10(4):513--526, 1998.

1628: 

1629: \bibitem{WaldenNerson94}

1630: Kim Wald{\'e}n and Jean-Marc Nerson.

1631: \newblock {\em Seamless Object-Oriented Software Architecture - Analysis and

1632:   Design of Reliable Systems}.

1633: \newblock Prentice-Hall, Inc., 1994.

1634: 

1635: \bibitem{Wendorff99}

1636: P.~Wendorff.

1637: \newblock Linking concepts to identifiers in information systems engineering.

1638: \newblock In S.~Sarkar and S.~Narasimhan, editors, {\em Proceedings of the

1639:   Ninth Annual Workshop on Information Technologies and Systems}, pages 51--56,

1640:   1999.

1641: 

1642: \bibitem{Wendorff01}

1643: P.~Wendorff.

1644: \newblock A formal approach to the assessment and improvement of terminological

1645:   models used in information systems engineering.

1646: \newblock In {\em Proceedings of the Joint Eighth European Software Engineering

1647:   Conference (ESEC) and Ninth {ACM SIGSOFT} Symposium on the Foundations of

1648:   Software Engineering ({FSE}-9)}, volume~26 of {\em Software Engineering

1649:   Notes}, pages 83--87, 2001.

1650: 

1651: \bibitem{Wille92}

1652: R.~Wille.

1653: \newblock Concept lattices and conceptual knowledge systems.

1654: \newblock {\em Computers and Mathematics with Applications}, 23(6-9):493--515,

1655:   1992.

1656: 

1657: \bibitem{Wille97}

1658: R.~Wille.

1659: \newblock Conceptual graphs and formal concept analysis.

1660: \newblock {\em Conceptual Structures: Fulfilling Peirce's Dream},

1661:   1257:290--303, 1997.

1662: 

1663: \end{thebibliography}

1664: 

1665: %======================================================================

1666: 

1667: %\newpage

1668: \appendix

1669: 

1670: %======================================================================

1671: \section{Semantic Properties Summary}

1672: 

1673: \begin{table}[htbp]

1674:   \caption{The Full Set of Semantic Properties}

1675:   \label{tab:The_Full_Set_of_Semantic_Properties}

1676:   \begin{center}

1677:     \begin{tabular}{|ccc|}

1678:       \hline

1679:       \textbf{Meta-Information:} & \textbf{Contracts}    & \textbf{Versioning} \\

1680:       author                     & ensure                & version \\

1681:       bon                        & generate              & deprecated \\

1682:       bug                        & invariant             & since \\

1683:       copyright                  & modifies              & \textbf{Documentation} \\

1684:       description                & require               & design \\

1685:       history                    & \textbf{Concurrency}  & equivalent \\

1686:       license                    & concurrency           & example \\

1687:       title                      & \textbf{Usage}        & see \\

1688:       \textbf{Dependencies}      & param                 & \textbf{Miscellaneous} \\

1689:       references                 & return                & guard \\

1690:       use                        & exception             & values \\

1691:       \textbf{Inheritance}       & \textbf{Pending Work} & time-complexity \\

1692:       hides                      & idea                  & space-complexity \\

1693:       overrides                  & review                &  \\

1694:                                  & todo                  &  \\

1695:       \hline

1696:     \end{tabular}

1697:   \end{center}

1698: \end{table}

1699: 

1700: %======================================================================

1701: % Fin

1702: 

1703: \end{document}

1704: 

1705: %%% Local Variables: 

1706: %%% mode: latex

1707: %%% TeX-master: t

1708: %%% End: 

1709: 

1710: % LocalWords:  Nerson's BON's EiffelCase BonBon BONBAZ Phillips's Ostroff ISE's

1711: % LocalWords:  PaigeOstroff Ostroff's Lancaric Kaminskaya's Lancaric's Kiniry's

1712: % LocalWords:  Kaminskaya EiffelStudio OOSC LeavensBakerRuby Reto Cheong's CWEB

1713: % LocalWords:  Felliason's Findler programmatically Javadoc param FreshMeat

1714: % LocalWords:  freshmeat Javadoc's html semant AFOSR MURI LeavensEtal

1715: