| products/Sources/formale Sprachen/Isabelle/Pure/Thy/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: TestTraffic.vdmrt Sprache: ScalaOriginal von: VDM© |
|
||||||
|
\section{Formal Specifications}
\begin{vdm_al} module GRAPH exports all definitions types Point :: xcoord : nat ycoord : nat; LineSegment :: end1 : Point end2 : Point inv mk_LineSegment(end1, end2) == end1 <> end2; Circle :: center : Point radius : nat1; Ellipse :: center : Point xradius : nat1 yradius : nat1; Polygon :: vertices : seq1 of Point inv mk_Polygon(points) == len points > 2; Polyline :: vertices : seq1 of Point inv mk_Polyline(points) == len points > 1; Box :: corner1 : Point corner2 : Point inv mk_Box(corner1, corner2) == corner1.xcoord <> corner2.xcoord and corner1.ycoord <> corner2.ycoord; ArcBox :: box : Box cornerradius : nat1; Text :: frame : Box startpoint : Point string : seq of char inv mk_Text(frame, startpoint, string) == abs (frame.corner1.ycoord - frame.corner2.ycoord) >= 20 and point_within_box(startpoint, frame) and (frame.corner1.ycoord < frame.corner2.ycoord and startpoint.ycoord + len(string) * 10 <= frame.corner2.ycoord or frame.corner1.ycoord > frame.corner2.ycoord and startpoint.ycoord + len(string) * 10 <= frame.corner1.ycoord); Compound :: frame : Box components : seq1 of Object inv mk_Compound(frame, components) == forall obj in set elems components & object_within_box(obj, frame); Object = Circle | Ellipse | Polygon | Polyline | Box | ArcBox | Text | Compound; Message = <SUCCESS> | <NOT_FIT> | <TEXT_NOT_FIT> | <NO_COMPONENT> | <NOT_COMPOUND> | <ERROR_FRAME_SIZE> | <ERROR_START_POINT> | <ERROR_NUM_VERTICES> \end{vdm_al} \begin{vdm_al} state GraphEditor of DRAWING_AREA : Box OBJECTS : seq of Object inv mk_GraphEditor(drawing_area, objects) == drawing_area.corner1.xcoord = 0 and drawing_area.corner1.ycoord = 0 and drawing_area.corner2.xcoord = 500 and drawing_area.corner2.ycoord = 350 and forall object in set elems objects & object_within_box(object, drawing_area) init mk_GraphEditor(drawing_area, objects) == drawing_area.corner1.xcoord = 0 and drawing_area.corner1.ycoord = 0 and drawing_area.corner2.xcoord = 500 and drawing_area.corner2.ycoord = 350 and objects = [] end \end{vdm_al} \begin{vdm_al} functions point_on_line : Point * LineSegment +> bool point_on_line(point, line) == (point.xcoord - line.end2.xcoord) * (line.end1.xcoord - line.end2.xcoord) > 0 and (point.xcoord - line.end2.xcoord) < (line.end1.xcoord - line.end2.xcoord) and (point.xcoord - line.end2.xcoord) * (line.end1.ycoord - line.end2.ycoord) = (line.end1.xcoord - line.end2.xcoord) * (point.ycoord - line.end2.ycoord); point_on_circle : Point * Circle +> bool point_on_circle(point, circle) == (circle.center.xcoord - point.xcoord) ** 2 + (circle.center.ycoord - point.ycoord) ** 2 = circle.radius ** 2; point_on_ellipse : Point * Ellipse +> bool point_on_ellipse(point, ellipse) == ellipse.yradius ** 2 * (ellipse.center.xcoord - point.xcoord) ** 2 + ellipse.xradius ** 2 * (ellipse.center.ycoord - point.ycoord) ** 2 = ellipse.xradius ** 2 * ellipse.yradius ** 2; point_on_polygon : Point * Polygon +> bool point_on_polygon(point, polygon) == exists index in set inds polygon.vertices & point_on_line(point, mk_LineSegment (polygon.vertices(index), polygon.vertices(index mod len polygon.vertices + 1))); point_on_polyline : Point * Polyline +> bool point_on_polyline(point, polyline) == exists index in set {i | i : nat1 & i in set inds polyline.vertices and i <> len polyline.vertices} & point_on_line(point, mk_LineSegment (polyline.vertices(index), polyline.vertices(index + 1))); point_on_box : Point * Box +> bool point_on_box(point, box) == (((((point.xcoord >= box.corner1.xcoord) and (point.xcoord <= box.corner2.xcoord)) or ((point.xcoord >= box.corner2.xcoord) and (point.xcoord <= box.corner1.xcoord))) and ((point.ycoord = box.corner1.ycoord) or (point.ycoord = box.corner2.ycoord))) or ((((point.ycoord >= box.corner1.ycoord) and (point.ycoord <= box.corner2.ycoord)) or ((point.ycoord >= box.corner2.ycoord) and (point.ycoord <= box.corner1.ycoord))) and ((point.xcoord = box.corner1.xcoord) or (point.xcoord = box.corner2.xcoord)))); point_on_arcbox : Point * ArcBox +> bool point_on_arcbox(point, arcbox) == point_on_box(point, arcbox.box); point_on_text : Point * Text +> bool point_on_text(point, text) == point_within_box(point, text.frame); point_on_compound : Point * Compound +> bool point_on_compound(point, compound) == point_on_box(point, compound.frame); point_on_object : Point * Object +> bool point_on_object(point, object) == (is_Circle(object) and point_on_circle(point, object)) or (is_Ellipse(object) and point_on_ellipse(point, object)) or (is_Polygon(object) and point_on_polygon(point, object)) or (is_Polyline(object) and point_on_polyline(point, object)) or (is_Box(object) and point_on_box(point, object)) or (is_ArcBox(object) and point_on_box(point, object.box)) or (is_Text(object) and point_within_box(point, object.frame)) or (is_Compound(object) and point_on_box(point, object.frame)); point_within_box : Point * Box +> bool point_within_box(point, box) == ((point.xcoord > box.corner1.xcoord and point.xcoord < box.corner2.xcoord) or (point.xcoord > box.corner2.xcoord and point.xcoord < box.corner1.xcoord)) and ((point.ycoord > box.corner1.ycoord and point.ycoord < box.corner2.ycoord) or (point.ycoord > box.corner2.ycoord and point.ycoord < box.corner1.ycoord)); circle_within_box : Circle * Box +> bool circle_within_box(circle, box) == point_within_box(mk_Point(circle.center.xcoord + circle.radius, circle.center.ycoord), box) and point_within_box(mk_Point(circle.center.xcoord - circle.radius, circle.center.ycoord), box) and point_within_box(mk_Point(circle.center.xcoord, circle.center.ycoord + circle.radius), box) and point_within_box(mk_Point(circle.center.xcoord, circle.center.ycoord - circle.radius), box); ellipse_within_box : Ellipse * Box +> bool ellipse_within_box(ellipse, box) == point_within_box(mk_Point(ellipse.center.xcoord + ellipse.xradius, ellipse.center.ycoord), box) and point_within_box(mk_Point(ellipse.center.xcoord - ellipse.xradius, ellipse.center.ycoord), box) and point_within_box(mk_Point(ellipse.center.xcoord, ellipse.center.ycoord + ellipse.yradius), box) and point_within_box(mk_Point(ellipse.center.xcoord, ellipse.center.ycoord - ellipse.yradius), box); polygon_within_box : Polygon * Box +> bool polygon_within_box(polygon, box) == forall vertex in set elems polygon.vertices & point_within_box(vertex, box); polyline_within_box : Polyline * Box +> bool polyline_within_box(polyline, box) == forall vertex in set elems polyline.vertices & point_within_box(vertex, box); box_within_box : Box * Box +> bool box_within_box(box1, box2) == point_within_box(box1.corner1, box2) and point_within_box(box1.corner2, box2); object_within_box : Object * Box +> bool object_within_box(object, box) == (is_Circle(object) and circle_within_box(object, box)) or (is_Ellipse(object) and ellipse_within_box(object, box)) or (is_Polygon(object) and polygon_within_box(object, box)) or (is_Polyline(object) and polyline_within_box(object, box)) or (is_Box(object) and box_within_box(object, box)) or (is_ArcBox(object) and box_within_box(object.box, box)) or (is_Text(object) and box_within_box(object.frame, box)) or (is_Compound(object) and box_within_box(object.frame, box)); copy_point(point : Point, vector : LineSegment) newpoint : Point post newpoint.xcoord = point.xcoord + vector.end2.xcoord - vector.end1.xcoord and newpoint.ycoord = point.ycoord + vector.end2.ycoord - vector.end1.ycoord; copy_points(points : seq1 of Point, vector : LineSegment) newpoints : seq1 of Point post len points = len newpoints and forall i in set inds points & newpoints(i) = copy_point(points(i), vector); make_copy_object(obj : Object, vector : LineSegment) newobj : Object post (is_Circle(obj) and newobj = mk_Circle(copy_point(obj.center, vector), obj.radius)) or (is_Ellipse(obj) and newobj = mk_Ellipse(copy_point(obj.center, vector), obj.xradius, obj.yradius)) or (is_Polygon(obj) and newobj = mk_Polygon(copy_points(obj.vertices, vector))) or (is_Polyline(obj) and newobj = mk_Polyline(copy_points(obj.vertices, vector))) or (is_Box(obj) and newobj = mk_Box(copy_point(obj.corner1, vector), copy_point(obj.corner2, vector))) or (is_ArcBox(obj) and newobj = mk_ArcBox(mk_Box(copy_point(obj.box.corner1, vector), copy_point(obj.box.corner2, vector)), obj.cornerradius)) or (is_Text(obj) and newobj = mk_Text(mk_Box(copy_point(obj.frame.corner1, vector), copy_point(obj.frame.corner2, vector)), copy_point(obj.startpoint, vector), obj.string)) or (is_Compound(obj) and newobj = mk_Compound(mk_Box(copy_point(obj.frame.corner1, vector), copy_point(obj.frame.corner2, vector)), make_copy_objects(obj.components, vector))); make_copy_objects(objs : seq1 of Object, vector : LineSegment) newobjs : seq1 of Object post len newobjs = len objs and newobjs = [make_copy_object(o, vector) | o in seq objs] operations create_circle(center : Point, radius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre circle_within_box(mk_Circle(center, radius), DRAWING_AREA) post OBJECTS = [mk_Circle(center, radius)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not circle_within_box(mk_Circle(center, radius), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_ellipse(center : Point, xradius : nat1, yradius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre ellipse_within_box(mk_Ellipse(center, xradius, yradius), DRAWING_AREA) post OBJECTS = [mk_Ellipse(center, xradius, yradius)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not ellipse_within_box(mk_Ellipse(center, xradius, yradius), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_polygon(vertices : seq1 of Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre polygon_within_box(mk_Polygon(vertices), DRAWING_AREA) post OBJECTS = [mk_Polygon(vertices)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not polygon_within_box(mk_Polygon(vertices), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_polyline(vertices : seq1 of Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre polyline_within_box(mk_Polyline(vertices), DRAWING_AREA) post OBJECTS = [mk_Polyline(vertices)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not polyline_within_box(mk_Polyline(vertices), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_box(corner1 : Point, corner2 : Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) post OBJECTS = [mk_Box(corner1, corner2)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_arcbox(corner1 : Point, corner2 : Point, cornerradius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) post OBJECTS = [mk_ArcBox(mk_Box(corner1, corner2), cornerradius)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; create_text(corner1 : Point, corner2 : Point, startpoint : Point, string : seq of char) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) and abs (corner1.ycoord - corner2.ycoord) >= 20 and point_within_box(startpoint, mk_Box(corner1, corner2)) and (corner1.ycoord < corner2.ycoord and startpoint.ycoord + len(string) * 10 <= corner2.ycoord or corner1.ycoord > corner2.ycoord and startpoint.ycoord + len(string) * 10 <= corner1.ycoord) post OBJECTS = [mk_Text(mk_Box(corner1, corner2), startpoint, string)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT> FRAME_SIZE : abs (corner1.ycoord - corner2.ycoord) < 20 -> OBJECTS = OBJECTS~ and msg = <ERROR_FRAME_SIZE> START_POINT : not point_within_box(startpoint, mk_Box(corner1, corner2)) -> OBJECTS = OBJECTS~ and msg = <ERROR_START_POINT> TEXT_NOT_FIT : corner1.ycoord < corner2.ycoord and startpoint.ycoord + len(string) * 10 > corner2.ycoord or corner1.ycoord > corner2.ycoord and startpoint.ycoord + len(string) * 10 > corner1.ycoord -> OBJECTS = OBJECTS~ and msg = <TEXT_NOT_FIT>; create_compound_object(corner1 : Point, corner2 : Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) and exists object in set elems OBJECTS & object_within_box(object, mk_Box(corner1, corner2)) post let components : seq1 of Object = [o | o in seq OBJECTS~ & object_within_box(o, mk_Box(corner1, corner2))] in OBJECTS = [mk_Compound(mk_Box(corner1, corner2), components)] ^ [o | o in seq OBJECTS~ & not object_within_box(o, mk_Box(corner1, corner2))] and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(corner1, corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT> NO_COMPONENT : not exists object in set elems OBJECTS & object_within_box(object, mk_Box(corner1, corner2)) -> OBJECTS = OBJECTS~ and msg = <NO_COMPONENT>; select_object(click : Point) object : [Object] ext rd DRAWING_AREA : Box rd OBJECTS : seq of Object pre point_within_box(click, DRAWING_AREA) post object in set elems OBJECTS and point_on_object(click, object) and forall i in set {index | index : nat1, j : nat1 & index in set inds OBJECTS and index < j and OBJECTS(j) = object} & not point_on_object(click, OBJECTS(i)) errs NO_SELECT : not exists obj in set elems OBJECTS & point_on_object(click, obj) -> object = nil; decompose_compound_object(object : Object) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre is_Compound(object) and object in set elems OBJECTS post OBJECTS = object.components ^ [o | o in seq OBJECTS~ & o <> object] and msg = <SUCCESS> errs NOT_COMPOUND : not is_Compound(object) -> msg = <NOT_COMPOUND>; delete_object(object : Object) ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre object in set elems OBJECTS post OBJECTS = [o | o in seq OBJECTS~ & o <> object]; move_object(object : Object, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre object in set elems OBJECTS post let stold = mk_GraphEditor(DRAWING_AREA,OBJECTS~), stnew = mk_GraphEditor(DRAWING_AREA,OBJECTS) in is_Compound(object) and post_move_compound_object(object,vector,msg,stold,stnew) or not is_Compound(object) and post_move_simple_object(object,vector,msg,stold,stnew); move_simple_object(object : Object, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre object in set elems OBJECTS and not is_Compound(object) and object_within_box(make_copy_object(object, vector), DRAWING_AREA) post OBJECTS = [make_copy_object(object, vector)] ^ [o | o in seq OBJECTS~ & o <> object] and msg = <SUCCESS> errs NOT_FIT : not object_within_box(make_copy_object(object, vector), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; move_compound_object(compound : Compound, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre compound in set elems OBJECTS and object_within_box(make_copy_object(compound.frame, vector), DRAWING_AREA) post OBJECTS = [make_copy_object(compound, vector)] ^ [o | o in seq OBJECTS & o <> compound] and msg = <SUCCESS> errs NOT_FIT : not object_within_box(make_copy_object(compound.frame, vector), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; copy_object(object : Object, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre object in set elems OBJECTS post let stold = mk_GraphEditor(DRAWING_AREA,OBJECTS~), stnew = mk_GraphEditor(DRAWING_AREA,OBJECTS) in is_Compound(object) and post_copy_compound_object(object,vector,msg,stold,stnew) or not is_Compound(object) and post_copy_simple_object(object,vector,msg,stold,stnew); copy_simple_object(object : Object, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre object in set elems OBJECTS and not is_Compound(object) and object_within_box(make_copy_object(object, vector), DRAWING_AREA) post OBJECTS = [make_copy_object(object, vector)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not object_within_box(make_copy_object(object, vector), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; copy_compound_object(compound : Compound, vector : LineSegment) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre compound in set elems OBJECTS and is_Compound(compound) and object_within_box(make_copy_object(compound.frame, vector), DRAWING_AREA) post OBJECTS = [make_copy_object(compound, vector)] ^ OBJECTS~ and msg = <SUCCESS> errs NOT_FIT : not object_within_box(make_copy_object(compound.frame, vector), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_circle(circle : Circle, new_radius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre circle in set elems OBJECTS and circle_within_box(mk_Circle(circle.center, new_radius), DRAWING_AREA) post OBJECTS = [mk_Circle(circle.center, new_radius)] ^ [o | o in seq OBJECTS~ & o <> circle] and msg = <SUCCESS> errs NOT_FIT : not circle_within_box(mk_Circle(circle.center, new_radius), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_ellipse(ellipse : Ellipse, new_xradius : nat1, new_yradius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre ellipse in set elems OBJECTS and ellipse_within_box(mk_Ellipse(ellipse.center, new_xradius, new_yradius), DRAWING_AREA) post OBJECTS = [mk_Ellipse(ellipse.center, new_xradius, new_yradius)] ^ [o | o in seq OBJECTS~ & o <> ellipse] and msg = <SUCCESS> errs NOT_FIT : not ellipse_within_box(mk_Ellipse(ellipse.center, new_xradius, new_yradius), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_polygon(polygon : Polygon, new_vertices : seq1 of Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre polygon in set elems OBJECTS and len new_vertices = len polygon.vertices and polygon_within_box(mk_Polygon(new_vertices), DRAWING_AREA) post OBJECTS = [mk_Polygon(new_vertices)] ^ [o | o in seq OBJECTS~ & o <> polygon] and msg = <SUCCESS> errs NUM_VERTICES : len new_vertices <> len polygon.vertices -> OBJECTS = OBJECTS~ and msg = <ERROR_NUM_VERTICES> NOT_FIT : not polygon_within_box(mk_Polygon(new_vertices), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_polyline(polyline : Polyline, new_vertices : seq1 of Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre polyline in set elems OBJECTS and len new_vertices = len polyline.vertices and polyline_within_box(mk_Polyline(new_vertices), DRAWING_AREA) post OBJECTS = [mk_Polyline(new_vertices)] ^ [o | o in seq OBJECTS~ & o <> polyline] and msg = <SUCCESS> errs NUM_VERTICES : len new_vertices <> len polyline.vertices -> OBJECTS = OBJECTS~ and msg = <ERROR_NUM_VERTICES> NOT_FIT : not polyline_within_box(mk_Polyline(new_vertices), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_box(box : Box, new_corner1 : Point, new_corner2 : Point) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre box in set elems OBJECTS and box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) post OBJECTS = [mk_Box(new_corner1, new_corner2)] ^ [o | o in seq OBJECTS~ & o <> box] and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; resize_arcbox(arcbox : ArcBox, new_corner1 : Point, new_corner2 : Point, new_corner_radius : nat1) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre arcbox in set elems OBJECTS and box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) post OBJECTS = [mk_ArcBox(mk_Box(new_corner1, new_corner2), new_corner_radius)] ^ [o | o in seq OBJECTS~ & o <> arcbox] and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT>; edit_text(text : Text, new_corner1 : Point, new_corner2 : Point, new_start_point : Point, new_string : seq of char) msg : Message ext rd DRAWING_AREA : Box wr OBJECTS : seq of Object pre text in set elems OBJECTS and box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) and abs (new_corner1.ycoord - new_corner2.ycoord) >= 20 and point_within_box(new_start_point, mk_Box(new_corner1, new_corner2)) and (new_corner1.ycoord < new_corner2.ycoord and new_start_point.ycoord + len(new_string) * 10 <= new_corner2.ycoord or new_corner1.ycoord > new_corner2.ycoord and new_start_point.ycoord + len(new_string) * 10 <= new_corner1.ycoord) post OBJECTS = [mk_Text(mk_Box(new_corner1, new_corner2), new_start_point, new_string)] ^ [o | o in seq OBJECTS~ & o <> text] and msg = <SUCCESS> errs NOT_FIT : not box_within_box(mk_Box(new_corner1, new_corner2), DRAWING_AREA) -> OBJECTS = OBJECTS~ and msg = <NOT_FIT> FRAME_SIZE : abs (new_corner1.ycoord - new_corner2.ycoord) < 20 -> OBJECTS = OBJECTS~ and msg = <ERROR_FRAME_SIZE> START_POINT : not point_within_box(new_start_point, mk_Box(new_corner1, new_corner2)) -> OBJECTS = OBJECTS~ and msg = <ERROR_START_POINT> TEXT_NOT_FIT : new_corner1.ycoord < new_corner2.ycoord and new_start_point.ycoord + len(new_string) * 10 <= new_corner2.ycoord or new_corner1.ycoord > new_corner2.ycoord and new_start_point.ycoord + len(new_string) * 10 <= new_corner1.ycoord -> OBJECTS = OBJECTS~ and msg = <TEXT_NOT_FIT> end GRAPH \end{vdm_al} ¤ Dauer der Verarbeitung: 0.45 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
