?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=MIDAS%3A+A+Formally+Constructed+Virtual+Machine&rft.creator=Wright%2C+Stephen&rft.subject=Event-B+Examples&rft.description=MIDAS+(Microprocessor+Instruction+and+Data+Abstraction+System)+is+a+specification+of+an+Instruction+Set+Architecture+(ISA)+capable+of+executing+binary+images+compiled+from+the+C+language.+It+was+developed+to+demonstrate+a+methodology+for+formal+construction+of+various+ISAs+in+Event-B+via+a+generic+model.+It+is+intended+to+be+representative+of+typical+microprocessor+ISAs%2C+but+using+a+minimal+number+of+defined+instructions%2C+in+order+to+make+complete+refinement+practical.+The+intention+is+to+simplify+the+number+and+complexity+of+the+defined+instructions+at+the+cost+of+compiler+complexity%2C+run-time+performance+and+code+density%2C+without+compromising+representativeness.+There+are+two+variants%3A+a+stack-based+machine+and+a+randomly+accessible+register+array+machine.+The+two+variants+employ+the+same+instruction+codes%2C+the+differences+being+limited+to+register+file+behavior.&rft.publisher=Deploy&rft.date=2009-06-04&rft.type=DEPLOY+Interest+Group+Item&rft.type=NonPeerReviewed&rft.format=application%2Fzip&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F84%2F1%2FMidasBundle.rar&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F84%2F2%2FMidas_Deploy.pdf&rft.identifier=++Wright%2C+Stephen++(2009)+MIDAS%3A+A+Formally+Constructed+Virtual+Machine.++%5BDEPLOY+Interest+Group+Item%5D++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F84%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>