Analysis & Description of Endurants

176. To analyse and describe endurants means to first

177. examine those endurant which have yet to be so analysed and described 178. by selecting (and removing fromνps) a yet unexamined sort (by name);

179. then analyse and describe an endurant entity (ιp:P) of that sort — this analysis, when applied to composite parts, leads to the insertion of zero²or more sort names³;

180. then to analyse and describe the mereology of each part sort, 181. and finally to analyse and describe the attributes of each sort.

343

value

176. analyse and describe endurants:Unit→Unit 176. analyse and describe endurants()≡

177. while∼is empty(νps)do

178. let ηS = select and removeηS()in

179. analyse and describe endurant sort(ιs:S) end end;

180. for allηP^• ηP∈αps doanalyse and describe mereology(ιp:P)end 181. for allηP^• ηP∈αps doanalyse and describe attributes(ιp:P)end

Theιof Items 179, 180 and 181 are crucial. The domain analyser is focused on sortS(andP) and is “directed” (by those items) to choose (select) an endurant ιs (ιp) of that sort. The ability of the domain analyser to find such an entity is a measure of that person’s professional creativity.

344

1 Here ‘white board’ is a conceptual notion. It could be physical, it could be yellow “post-it” stickers, or it could be an electronic conference “gadget”.

2 If the sub-parts ofpare all either atomic or already analysed, then no new sort names are added to the repositoryνps).

3 These new sort names are then “picked-up” for sort analysis &c. in a next iteration of the while loop.

As was indicated in Chap. 2, the mereology of a part may involve unique identifiers of any part sort, hence must be done after all such part sort unique identifiers have been identi-fied. Similarly for attributes which also may involve unique identifiers Each iteration of anal-yse and describe endurant sort(ιp:P) involves the selection of a sort (by name) (which is that of either a part sort or a material sort) with this sort name then being removed.

182. The selection occurs from the global state (hence: ()) and changes that (hence Unit).

183. The affected global state component is that of the reservoir,νps.

345

value

182. select and removeηS:Unit→ηP 182. select and removeηS()≡

183. letηS^•ηS ∈νpsinνps :=νps\ {ηS} ;ηSend

The analysis and description of all sorts also performs an analysis and description of their possible unique identifiers (if part sorts) and attributes. The analysis and description of sort mereologies potentially requires the unique identifiers of any set of sorts. Therefore the analysis and description of sort mereologies follows that of analysis and description of all sorts. 346

184. To analyse and describe an endurant 185. is to find out whether it is a part.

186. If so then it is to analyse and describe it as a part, 187. else it is to analyse and describe it as a material.

184. analyse and describe endurant sort: (P|M)→Unit 184. analyse and describe endurant sort(e:(P|M))≡ 185. ifis part(e)

185. assert: is part(e)≡is endurant(e)∧is discrete(e) 186. thenanalyse and describe part sort(e:P)

187. else analyse and describe material parts(e:M) 184. end

Analysis & Description of Part Sorts ³⁴⁷ 188. The analysis and description of a part sort

189. is based on there being a set,ps, of parts⁴to analyse — 190. of which an archetypal one,p^′, is arbitrarily selected.

191. analyse and describe partp^′

188. analyse and describe part sort: P→Unit 188. analyse and describe part sort(p:P)≡ 189. let ps =observe parts(p)in 190. let p^′:P^•p^′∈psin

191. analyse and describe part(p^′) 188. end end

348

192. The analysis (&c.) of a part

193. first analyses and describes its unique identifiers.

194. If atomic 195. and

4 We can assume that there is at least one element of that set. For the case that the sort being analysed is a domain∆, say“The Transport Domain”,p^′is some representative“transport domain”δ. Similarly for any other sort for whichpsis now one of the sorts ofδ.

196. if the part embodies materials, 197. we analyse and describe these.

198. If not atomic then the part is composite 199. and is analysed and described as such.

349

192. analyse and describe part: P→Unit 192. analyse and describe part(p) ≡

193. analyse and describe unique identifier(p) ; 194. if is atomic(p)

195. then

196. ifhas materials(p)

197. thenanalyse and describe part materials(p)end 198. else assert:is composite(p)

199. analyse and describe composite endurant(p)end 192. pre:is discrete(p)

We do not associate materials with composite parts.

Analysis & Description of Part Materials 350

200. The analysis and description of the material part sorts, one or more, of atomic partspof sort Pcontaining such materials,

201. simply observes the material sorts of p,

202. that is generates the one or more continuous endurants 203. and the corresponding observer function text.

204. The reservoir of sorts to be inspected is augmented by the material sorts — except if already previously entered (the\ αpsclause).

200. analyse and describe part materials: P→Unit 200. analyse and describe part materials(p)≡ 201. observe material sorts(p) :

202. τ := τ ⊕[ ”typeM1,M2,...,Mm;

203. valueobs M1:P→M1,obs M2:P→M2,...,obs Mm:P→Mm;” ] 204. νps := νps⊕ ([ M1,M2,...,Mm ]\ αps)

200. pre:has materials(p)

Analysis & Description of Material Parts 351

205. To analyse and describe materials,m, i.e., continuous endurants, 206. is only necessary ifmhas parts.

207. Then we observe the sorts of these parts.

208. The identified part sort names update both name reservoirs.

205. analyse and describe material parts: M→Unit 205. analyse and describe material parts(m:M)≡ 206. ifhas parts(m)

207. thenobserve part sorts(m):

207. τ := τ ⊕[ ”typeP1,P2,...,PN ;

207. valueobsPi: M→Pi i:{1..N};” ] 208. k νps := νps ⊕([ ηP1,ηP2,...,ηPN ]\ αps) 208. k αps := αps⊕[ ηP1,ηP2,...,ηPN ]

205. end

205. assert:is continuous(m)

Analysis & Description of Composite Endurants ³⁵² 209. To analyse and describe a composite endurant of sortP

210. is to (we choose first) to analyse and describe the unique identifier of that composite endurant, 211. then to analyse and describe the sort. If the sort has a concrete type

212. then we analyse and describe that concrete sort type 213. else we analyse and describe the abstract sort.

209. analyse and describe composite endurant: P→Unit 209. analyse and describe composite endurant(p)≡ 210. analyse and describe unique identifier(p) ; 211. if has concrete type(p)

212. thenanalyse and describe concrete sort(p) 213. else analyse and describe abstract sort(p)

211. end

Analysis & Description of Concrete Sort Types 353

214. The concrete sort type being analysed and described is 215. either

216. expressible by some compound type expression 215. or is

217. expressible by some alternative type expression.

214. analyse and describe concrete sort: P→Unit 214. analyse and describe concrete sort(p:P)≡

216. analyse and describe concrete compound type(p) 215. ⌈⌉

217. analyse and describe concrete alternative type(p) 214. pre:has concrete type(p)

354

218. The concrete compound sort type

219. is expressible by some simple type expression, T=E(Q,R,...,S) over either concrete types or existing or new sorts Q, R, ..., S.

220. The emerging sort types are identified 221. and assigned to bothνps

222. and αps.

355

216. analyse and describe concrete compound type: P →Unit 216. analyse and describe concrete compound type(p:P) ≡ 218. observe part type(p):

218. τ := τ ⊕[ ”typeQ,R,..,S, T =E(Q,R,...,S);

218. valueobsT: P →T ;” ] ; 219. let {Pa,Pb,...,Pc}= sorts of({Q,R,...,S}) 220. assert: {Pa,Pb,...,Pc} ⊆ {Q,R,...,S} in 221. νps :=νps⊕[ηPa,ηPb,...,ηPc]k

222. αps :=αps⊕([ηPa,ηPb,...,ηPc] \αps)end 216. pre:has concrete type(p)

356

223. The concrete alternative sort type expression

224. is expressible by an alternative type expression T=P1|P2|...|PN where each of the alternative types is made disjoint wrt. existing types by means of the description languagePi::mkPi(su:Pi) construction.

225. The emerging sort types are identified and assigned 226. to bothνps

227. and αps.

357

217. analyse and describe concrete alternative type: P →Unit 217. analyse and describe concrete alternative type(p:P) ≡ 223. observe part type(p):

224. τ := τ ⊕[ ”typeT=P1|P2|...| PN, Pi::mkPi(s u:Pi) (1≤i≤N);

224. valueobsT: P→T ;” ] ; 225. let {Pa,Pb,...,Pc}= sorts of({Pi|1≤i≤n}) 225. assert: {Pa,Pb,...,Pc} ⊆ {Pi|1≤i≤n}in 226. νps :=νps⊕([ηPa,ηPb,...,ηPc]\ αps)k 227. αps :=αps⊕[ηPa,ηPb,...,ηPc]end 214. pre:has concrete type(p)

Analysis & Description of Abstract Sorts ³⁵⁸ 228. To analyse and describe an abstract sort

229. amounts to observe part sorts and to 230. update the sort name repositories.

228. analyse and describe abstract sort: P→Unit 228. analyse and describe abstract sort(p:P)≡ 229. observe part sorts(p):

229. τ := τ ⊕[ ”typeP1, P2,..., Pn;

229. valueobs Pi:P→Pi (0≤i≤n);” ] 230. k νps := νps ⊕([ηP1,ηP2,...,ηPn]\αps) 230. k αps :=αps⊕[ηP1,ηP2,..., ηPn]

Analysis & Description of Unique Identifiers 359

231. To analyse and describe the unique identifier of parts of sortPis 232. to observe the unique identifier of parts of sortP

233. where we assume that all parts have unique identifiers.

231. analyse and describe unique identifier: P→Unit 231. analyse and describe unique identifier(p)≡ 232. observe unique identifier(p):

232. τ := τ ⊕[ ”typePI;valueuid P:P→PI;” ] 233. assert: has unique identifier(p)

Analysis & Description of Mereologies ³⁶⁰ 234. To analyse and describe a part mereology

235. if it has one

236. amounts to observe that mereology 237. and otherwise do nothing.

238. The analysed quantity must be a part.

234. analyse and describe mereology: P→Unit 234. analyse and describe mereology(p)≡ 235. ifhas mereology(p)

236. thenobserve mereology(p) :

236. τ := τ ⊕ ”typeMT =E(PIa,PIb,...,PIc) ;

236. valuemereo P: P→MT ;”

237. else skip end 234. pre:is part(p)

Analysis & Description of Part Attributes 361

239. To analyse and describe the attributes of parts of sortPis 240. to observe the attributes of parts of sortP

241. where we assume that all parts have attributes.

239. analyse and describe part attributes: P →Unit 239. analyse and describe part attributes(p)≡ 240. observe attributes(p):

240. τ := τ ⊕[ ”typeA1, A2,..., Am;

240. valueattrA1:P→A1,attr A2:P→A2,...,attrAm:P→Am;” ] 241. assert: has attributes(p)

In document Dines Bjørner From Domains to Requirements (Sider 86-91)