.Open Simple Graphics POSITION::=Net{ x,y:Nat0 }, pixels::=\$ \$POSITION. To make this treatment simpler, assume that we can work with a logical window that is unlimitted and delay tackling problems of graphics leaving the physical `screen` or display. There exist well techniques for doing this any way. For p: pixels, neighbours(p) ::@pixels={n:pixels || p.x-1<=n.x<=p.x+1 and p.y-1<=n.y<=p.y+1}. For p,q: pixels, p next_to q::@=q in neighbours(p). ()|- (g0): next_to in Reflexive(pixels) & Symmetric(pixels)~transitive(pixels). . Proof of g0 Reflexive and Symmetric follow by substitution of definitions and rearrangement. Lack of transitivity comes form considering pixels (0,1),(0,2),(0,3). For S:@pixels, outside(S) ::@pixels=pixels~S, close(S) ::@pixels= |neighbours(S), inside(S) ::@pixels= outside(close(outside(S))), edge(S) ::@pixels=close(S)~inside(S). colors::={white, black, ...}. pictures::=pixels->colors For o:{+,-, div, mod, *, /}, o::infix(pixels) = (x=>(1st).x o (2nd).x, y=>(1st).y o (2nd).y). ()|- (g1): For a,b:pixels, o:{+,-, div, mod, *, /}, a o b = (x=>a.x o b.x, y=>a.y o b.y). For a:pixels, n:Real, n * a ::pixels= (x=> round(n * a.x), y=> round(n * a.y) ). ()|- (g2): MODULE(M=>pixels, Ring=>Reals). WIDTH_DEPTH::=Net{ w, d:Numbers&positive, width:=w, depth:=d. wd:=(x=>w,y=>d)}. PATTERN::=Net{ WIDTH_DEPTH. basis::\$ \$POSITION and {0<=x<=w, 0<=y<=d} ->colors. cycle::=(x=>w+1, y=>d+1). color::points->colors=map[p:points](basis(p mod cycle)) }=::PATTERN. pattern::={none} \/ \$ \$PATTERN. RECTANGLE::=Net{ WIDTH_DEPTH. tl, tr, br, bl, c::pixels, top_left::=tl, top_right::=tr, bottom_right::=br, bottom_left::=tr, center::=c. centre::=center. br=tl+wd. c = tl + 0.5*wd. l:=left::=tl.x, l=bl.x, r:=right::=tr.x, r=br.x, t:=top:=tl.y, t=tr.y, b:=bottom::=bl.y, b=br.y. coverage::={p:pixels || tl.x<=p.x<=tr.x and tl.y<=p.y<=br.y} }=::RECTANGLE. GRAPHIC::=Net{ coverage::@pixels, - part filled with pattern contacts::@coverage, - pixels where it can touch another graphic. shape::Sets, fill, pen::pattern, type::{line,box,...}. (gt1): type=line iff LINE. (gt2): type = box iff BOX. .Hole }=::GRAPHIC. graphics::@\$ \$GRAPHIC. THIN::=Net{ GRAPHIC. inside={}}. LINE::=Net{ start, end::pixels. |-(gl0): GRAPHIC and Net{type=line}. |-(gl1): contacts={start, end}. |-(gl2): for all p,q in coverage. p do(next_to) q. |-(gl3): shape={horizontal, vertical, straight, curved,...}. |-(gl4): pen=fill. arrow_heads::@{start,finish,middle}><{open,closed}><{hollow, thin, thick,...}. }=::LINE. BOX::=Net{ RECTANGLE. Assume that there are no holes or projections. Boxes are supposed to cover a rectangular area. |-(gb0):GRAPHIC and Net{type=box}. |-(gb1):contacts=edge(coverage). |-(gb2):shape={rectangle, text, char, blob}. }=::BOX. touches::Reflexive(graphics). |-(g4): PART_WHOLE(graphics, is_part_of). |-(g5): for all g1,g2:graphics, if g1 touches g2 then not g1 is_part_of g2. |-(g6): for all g1,g2:graphics, if g1 is_part_of g2 then coverage(g1)==>coverage(g2)). |-(g7): for all g1,g2:graphics, g1 overlaps g2::@ =some coverage(g1)& coverage(g2)). |-(g8): for all g1,g2:graphics, if not g1 (is_part_of | /is_part_of) g2 then not g1 overlaps g2 ). |-(g9): for all g1,g2:graphics, if g1 touches g2 then some close contacts(g1) & close contacts(g2). above::@(qraphics,graphics)=rel[a,b](b.l<=a.l and a.r<=b.r and a.c.y>b.c.y), below::@(qraphics,graphics)= /above. left::@(graphics,graphics)=rel[a,b](a.t<=b.t and a.b>=b.b and a.c.x