range - Formal methods - Map of price relating cars to price with two sets BL and Fiat -

-

i have question chapter 5 in practical formal methods vdm derek andrews , darrel ince unsure how answer, here is, help!

if map price relates cars price, set bl contains cars made british leyland , fiat cars made fiat. write down following descriptions using map facilities , set facilities described in chapter , chapter on sets.

(d) number of fiat cars have price between £6000 , £7000

this think far...

1.get prices of fiats i.e. price(fiat) returning subset of price map

i.e. {punto -→ 5500, panda -→ 6600}

2.possibly card on map restriction on range of price(fiat)...

   **{6000...7000} ◁ rng price(fiat)**

but not sure legal

  1. i think function application not need subset of price map, want restrict map domain of fiats, let's use domain restriction:

    fiat <: price

    that should yield {punto → 5500, panda → 6600}

  2. now want subset of prices (the right side, i.e. range) restricted 6000..7000:

    (fiat <: price) :> {6000,...,7000}

    that gives set of couples (fiat,price) prices in given interval.

  3. apply cardinality operator result number of found cars.

(caveat: i'm not familiar vdm underlying logic should quite same in vdm, b, z, etc. did not check if used syntax above correct.)

edit: fixed syntax of interval, nick's answer.


Comments

Post a Comment

Popular posts from this blog

c++ - OpenCV Error: Assertion failed <scn == 3 ::scn == 4> in unknown function, -

-
i read alot other solution still confused should mine... #include <opencv2/objdetect/objdetect.hpp> #include <opencv2/highgui/highgui.hpp> #include <opencv2/imgproc/imgproc.hpp> #include <iostream> #include <stdio.h> using namespace std; using namespace cv; int main(int argc, const char** argv) { //create cascade classifier object used face detection cascadeclassifier face_cascade; //use haarcascade_frontalface_alt.xml library face_cascade.load("haarcascade_frontalface_alt.xml"); //setup video capture device , link first capture device videocapture capturedevice; capturedevice.open(0); //setup image files used in capture process mat captureframe; mat grayscaleframe; //create window present results namedwindow("outputcapture", 1); //create loop capture , find faces while (true) { //capture new image frame capturedevice >> captureframe; ...
Read more

php - render data via PDO::FETCH_FUNC vs loop -

-
i've been using 2 methods render data. the first one: function name($id,$name){ return '<div id="'.$id.'">'.$name.'</div>'; } echo implode($pdo->query("select id,name user")->fetchall(pdo::fetch_func,'name')); the second one: $users = $pdo->query("select id,name user")->fetchall(pdo::fetch_obj); foreach($users $user){ echo name($user->id,$user->name); } i don't understand how pdo::fetch_func works. tried figure out. however, not well-documented. could please explain fetch mode? , also, 1 performs better? thank you. both methods wrong , have learn how use templates , how separate business logic presentation logic. $users = $pdo->query("select id,name user")->fetchall(pdo::fetch_obj); tpl::assign('users', $users); is code business logic part. then in template <?php foreach $users $row): ?> <div id="<?=$...
Read more

The canvas has been tainted by cross-origin data in chrome only -

-
uncaught securityerror: failed execute 'getimagedata' on 'canvasrenderingcontext2d': canvas has been tainted cross-origin data i getting above error in chrome. code(following) works fine in mozilla. have not corss domain issue. why above error in chrome? var wheel_canvas, wheel_context, can_w, can_h, wheel_grd; var large_radius = 160; var small_radius = 120; var wheel_canvas = document.getelementbyid('wheel_canvas'); var wheel_context = wheel_canvas.getcontext('2d'); var can_w = $(wheel_canvas).width(); var can_h = $(wheel_canvas).height(); var centerx = can_w / 2, centery = can_h / 2; var wheel_grd = null; test('#ff0000'); function test(hex) { $('#clrpicker').css({'left': 210, 'top': 210 }); inverted = hexbw(hex); $('#color_val_show').val(hex); current_color_hex_val_selected = hex; $('#color_val_show').css({'color':inverted,'background':hex}); fillgradient...
Read more