Example Database query

SynthesisofCo[e-mail]¨URINFORMATIKIIAachenOverviewMotivation:FormalSpecificationsMessageSequenceChartsGeneratingSkeletonsInterfaces&TypesConclusionSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—2MotivationConcurrentProgrammingPart1:Specification-SpecificationLanguage-RequiredProperties-FormalVerificationPart2:ImplementationConcurrentframework:Either:“Manual”codegenerationOr:AutomatedprogramgenerationCommunication-independentcomputationsSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—3StatusQuo:ConcurrencyMethodologiesC/C++PosixThreads(MPI,PVM)ErlangMailboxJavaSharedmemory&synchronizationJavaSpacesJavaMessageService(JMS)ConcurrentHaskellSharedmemory&synchronizationMessagePassingSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—4ConcurrentHaskellPrimitivesConcurrencyprimitivesembeddedintoIOmonadbe-causeofnondeterministicinterleavingNewthread:forkIO::IO()-IOThreadIdFIFOchannels:newChan::IO(Chana)writeChan::Chana-a-IO()readChan::Chana-IOaSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—5GraphicalRepresentations,ToolsMessageSequenceChartsLiveSequenceChartsSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—6MessageSequenceCharts*AufgabePR/GRDatatypes/datalanguageSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—7Example:DatabasequeryClientServerinput:=getQueryFromUser()Query(q:=input)r:=doDBQuery(q)whenfound(r)Found(r)otherwiseNotFoundaltdisplayResult()mscDBQuerySynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—8BasicMSCsmscSimple;instp1;instp2;p1:instance;outChallenge(c)top2;inResponse(r)fromp2;endinstance;p2:instance;inChallenge(c)fromp1;outResponse(r)top1;endinstance;endmsc;p1p2Challenge(c)Response(r)mscSimplePhraseRepresentation(MSC/PR)forautomatedprocessingGraphicalRepresentation(MSC/GR)forvisualisationSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—9InlineExpressionsABCMwhenexpr1N1whenexpr2N2altloop1,10mscInlineTwomaintypes:LoopsAlternatives(2ormore)SynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—10ReferencesABCKNgCompLmscAppABMNgOmscCompReferencesallowmodularisationReferencedinstancesmustexistinsubchartGatesallowcommunicationto/fromsubchartSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—11IssuesGenerateexecutablecodeType-safecommunicationCompositionExtensibilityNondeterminismSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—12MappingMSCstoHaskellInstances≃ProcessesInstanceeventsareregularIOactionsProcessesproceedindependentlyuntilsynchronizationrequiredActionsprovideextensibilityMessagePassing≃ConcurrentHaskellAPITrade-off:ChannelperSender/Recipient-pairprovideslimitedtypingbutbetterhandlingSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—13CommunicationABMNV5gmscSimplemoduleSimpledataAToB=M|NdataBToG=VIntdataSimpleS=SimpleS{aTob::ChanAtoB,bTog::ChanBtoG}init::IOSimpleSinit=doaToB-newChanbToG-newChanreturnSimpleS{aToB=aToB,bToG=bToG}main::IO()main=dosimpleS-initrunProcessprocessAsimpleSrunProcessprocessBsimpleSSteps:1.Collectmessageconstructorsforeachsender/receiverpair2.Createchannels3.StartprocessesSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—14ValuesandActionsABx:=5Data(v:=x+1)mscMessagesprocessA::...-MIOStateAS()processA...=doget=\st-putst{x=5}x-getsxsendaToB(Data(x+1))processB::...-MIOStateBS()processB...=doSynv-receiveaToBget=\st-putst{v=v}Components:BindingpartExpressionpartSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—15ValuesandActionsABx:=5Data(v:=x+1)mscMessagesprocessA::...-MIOStateAS()processA...=doget=\st-putst{x=5}x-getsxsendaToB(Data(x+1))processB::...-MIOStateBS()processB...=doSynv-receiveaToBget=\st-putst{v=v}Components:BindingpartExpressionpartSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—15ValuesandActionsABx:=5Data(v:=x+1)mscMessagesprocessA::...-MIOStateAS()processA...=doget=\st-putst{x=5}x-getsxsendaToB(Data(x+1))processB::...-MIOStateBS()processB...=doSynv-receiveaToBget=\st-putst{v=v}Components:BindingpartExpressionpartTypechecked:MessageConstructorAssignmentsTransmittedValuesSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—15PassingControl:ModularityReferencespasscontroltoanembeddedMSCs.ABCKNgCompLmscAppprocessA=dosendaTobKcallComp.processAsendaTobLprocessB=doK-receiveaTobcallComp.processBL-receiveaTobprocessC=doComp.N-receivegTocSynchronousconcatenation:AllinstancesenterMSCsimultaneouslyAsynchronousconcatenation:MSCsproceedindependently(untilsynchronisationisrequired)SynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts—16PassingControl:ExtensibilityPf(x,2)mscExtendExtend.hs:moduleExtendprocessP=dox-getsxExtendP.fx2ExtendP.hs:moduleExtendPf::T1-T2-MIOStatePS()farg1arg2=do...UsesHaskell’sModule-conceptTypesT1,T2knownattranslationtimeProgrammercanaccessstatefromactionsSynthesisofConcurrentHaskellprogramsfromMessageSequenceCharts