Og endelig er vi da ved den ``go'e gamle'' programmering. Det som de fleste forstår ved datalogi. Men også her spiller abstraktion og trinvis forfining af sådanne abstraktioner mod konkret, eksekverbar kode, en alt afgørende rolle. Evnen til at abstrahere, og til sikkert, ubesværet og forståeligt at nedskrive abstraktioner, denne evne er helt central for den praktiserede datalog's success. Meget kan læres, men ikke alt. En del tilbagestår som en kunst. I det følgende vil jeg forsøge opridse blot nogle få af de mange overvejelser datalogen må gøre sig i det daglige arbejde, og for hvilken der derfor finder en løbende forskning sted, også på IT/DTU.
Ved abstraktion forstår vi det at fokusere på visse egenskaber ved en genstand samtidig med at der således ses bort fra andre egenskaber. De første ``udnævnes'' til at være de væsentlige, de andre at være ``mindre betydningsfulde''. Ved abstrakt modellering forstår vi det at finde et passende matematisk model eller et passende matematisk logisk udsagn der beskriver den eller de udnævnte, vigtige egenskaber.
Som dataloger betjener vi os af abstraktion som et bedste middel til at betvinge kompleksitet af systemer. Ved at abstrahere kan vi troværdigt tackle endog de største systemer. Matematikken tilbyder de hidtil eneste midler til utvetydigt at abstrahere.
Et jernbanespor modelleres f.eks. som et ikke nærmere beskrevet matematisk objekt der siden, algebraisk, kan udbygges med en række egenskaber. Først, f.eks., at sporet kan besidde et antal sammenføjningspunkter. Et par skinner har således to: et i hver ende. Et almindeligt sporskifte tre. Et kryds fire. Sammenføjningspunkterne defineres passende abstrakt således at det er enkelt at tale om kombinationer af skinner, som for et Märklin sæt. Dernæst tilføjes egenskab af en skinnetilstand således at vi kan tale om åbne og lukkede sporstrækninger. Nu indføres tog som værende noget abstrakt noget, der (blot) er positioneret [knyttet], i tid, over [til] en sekventiel (sammenhængende) serie skinner. Osv. Altsammen alene karakteriseret ved matematiske (herunder især matematisk logiske) egenskaber snarere end ved grafteoretiske, kombinatoriske eller operationsanalytiske egenskaber. Disse senere tilkommer som en del af en muligvis afledt `jernbane'-teoridannelse. Funktioner over det abstrakte domæne (af f.eks. jernbaner) kan nu defineres som almindelige diskret-matematiske funktioner eller ved deres matematisk-logiske egenskaber (herunder ved axiomer).
Som nævnt tidligere kan man udtrykke abstraktioner algebraisk, denotationsmæssigt, operationelt, etc. Man kan tackle abstraktion på modelteoretiske eller på bevisteoretiske præmisser, og man kan kombinere disse.
Værktøjer -- til udvikling og syntaktisk, og iblandt semantisk, afprøvning, og ihvertfald analyse, af abstrakte specifikationer -- udgør en ret så avanceret datamatisk teknologi. Idet abstrakte specifikationer ofte er formuleret i et specifikationssprog, der tillader formulering af ikke-beregnelige systemer opstår således afprøvningsproblematikken: hvor går grænserne for, hvad der kan analyseres.
Dette sidste -- og mere generelt, principper og teknikker for konstruktion af abstraktioner -- er vigtige emner både i den datalogiske praksis som i dens udforskning.
Ved ID/DTH er der siden 1976 forsket og undervist i abstraktion og det næste emne (forfining). IT/DTU nyder internationalt en meget høj anseelse heri.
Abstraktionerne tillader os at separere væsentlige, ``evige'' egenskaber fra de af den til enhver tid gængse teknologibestemte egenskaber. Forfining fra abstraktioner mod konkrete realisationer er derfor styret udefra af øjeblikkelige teknologivalg og indefra af ønsket om korrekthed i relation til basale, vedvarende egenskaber.
Der findes i dag flere forfiningsteknikker. Man kan ``opfinde'' en forfining, eller man kan mekanisk transformere en abstraktion hen imod en konkretisering. De første teknikker benævnes ``invent & verify, posit & prove''. De sidste ``refinement calculi''.
Ved IT/DTU studeres begge facetter af formel udvikling.
De første kræver gode specifikationsværktøj, de sidste, foruden de forrige værtøj, kræver endvidere gode bevis- eller model-afprøvningsværktøj. Se punkt 3.2.4 nedenfor.
Som et eksempel på en forfining kan vi anføre flg.: som information kan man abstrahere en telefonbog som en matematisk funktion, en afbildning, fra abonnenters navne til deres adresser og telefonnumre. I en første konkretisering, i form af en algebraisk bestemt (dog stadig abstrakt) data type, opfattes en telefonbog som et binært træ. I roden af et vilkårligt træ er anført een abonnent, og disse abonnenter er spredt ud over det binære træ således at abonnenter i ``venstre'' undertræer kommer før, i en lexicografisk ordning, abonnenten i træets rod, og abonnenter i ``højre'' undertræer kommer efter. Man kan intuitivt forestille sig denne abstrakte data type -- hvis operationer (aflæs, indsæt, fjern, m.fl.) vi ikke skal berøre -- som det vi allerede har kaldt det: træer. Og vi kan derfor tegne et sådant, tilfældigt træ. Men bemærk: det er ikke et træ. Der er ikke noget lagerbegreb knyttet, endnu, til disse træer. Således er der ingen repræsentation for træets rødder, endsige grene. I næste trin bevæger vi os nu mod den teknologi, der muliggør at vi kan tale om lageradresser (pegere, lænker). Det gør vi ved at opfatte enhver rod i træet og dets undertræer som en post (record) med bl.a. følgende felter: abonnentdata (navne mv., adresser og telefonnumre), og ``venstre'' hhv.\ ``højre'' lænker. Disse peger på rødder i undertræer eller er ``tomme'' pegere, dvs. at roden er et blad! I dette trin af forfining kan vi opfatte også pegerne som algebraiske størrelser der, ligesom de almindelige operationer, er underkastet axiomer. Sluttelig afbilder vi denne abstrakt formulere model af en konkret datastruktur ind i det valgte programmeringssprog's datastrukturer.
Vi har antydet en fire trins forfining. Ofte kan en udvikling af en domænemodel indebære typisk et dusin forfiningstrin, en kravspecifikation tilsvarende et dusin trin, og endelig kan selve programmelkonstruktionen indebære op mod en snes sådanne trin. Vi taler altså typisk af størrelsesordenen 30-50 niveauer af abstraktion!
Korrekthed er ene afgørende. Hvor often hører vi ikke om at der er fejl i programmellet og at disse, foruden dybt at irritere dets daglige bruger, kan afstedkomme at raketter eksploderer, at operationspatienter dør under narkose, osv. Når man så betragter at det antal tilstande et mellemstort programmelsystem kræver 30-40 cifrede tal for at udtrykke deres antal, ja så kan man hurtigt aflede umuligheden af at afprøve sådant programmel for fejl. Det er faktisk nemmere -- kan man med større rimelighed påstå -- at udvikle det således at det apriori er korrekt: gennem at forstå domænet, forstå kravene og ved trinvist at udvikle disse og programmellet kan man komme et langt stykke. Det meste af resten kan man komme ved at føre formelle beviser og ved såkaldt model-afprøvning. Formelle bevismetoder kan mere end model-afprøvning. Model-afprøvning er mere eller mindre automatisk hvorimod et formelt bevis som oftest kræver at datalogen selv opstiller bevisstrategier og -taktikker.
Hvad der her er sagt lyder meget optimistisk. Virkeligheden, idag, 1997, er dog knap så rosenrød. Meget kan opnås hvad angår korrekthed, men fuld sikkerhed får man muligvis kun hos paven i Rom!
Man kan sige at korrekthed er et af datalogiens vigtigste hensyn: programmels fejlfrihed og teknikker og teorier herfor. Området bygger på både teoretisk datalogi og metodelære.
Værktøj til hjælp ved udvikling af beviser, subsidiært deres fulde automation, såvelsom model-afprøvningsværktøj hører til blandt den teknologisk set mest avancerede datamatik idag.
Der forskes mao. intensivt i dette område, også ved IT/DTU. Flere PhD afhandlinger omhandler dette.
De flg. definitioner er ret så diskutable, men tjener til at påpege vigtige forskningsovervejelser.
En lang række øvrige metodelære og systemanalyse principper, teknikker og værktøj er nødvendige for at sikre bl.a. følgende programmel- & systemfacetter:
Et systems (inklusive dets programmels') pålidelighed måles ved den sandsynlighed systemet har for at fejle -- målt f.eks. i relation til antal brug af systemfunktioner per år.
Her drejer det sig om at programmel, pga.\ svigt i tilgrænsende fysiske systemer, ikke, i sig selv medfører at det misforstår, herunder ikke opfatter disse svigt, med tab af menneskeliv eller ødelæggelse af vigtige resourcer.
Dvs. at programmelafvikling vedbliver selv i, på anden vis frembragt, fejlbehæftede situationer. Tilgangsproblematikken sikres som oftest ved replicering af maskinel.
Troværdigheds-facetter udgør et sandt eldorado for udforskning. Dels er der et stort økonomisk betinget behov for sikrere metoder, dels er emnerne rimeligt skarpt afgrænsede.
Med ID/DTH's ProCoS projekt er der ved DTH, nu ved IT/DTUs SEKTION FOR DATAMATBASEREDE SYSTEMER, og særlig begrundet i professor Zhou Chaochen's, lektor Hans Rischel's og docent Ander P. Ravn's arbejde, forsket og undervist i dette helt centrale område. Problematikken er langt fra afklaret.
Lad os postulere begrebet ikke-autoriserede brugere.
Et datamatisk system er ultimativt sikkert såfremt en ikke-autoriseret bruger som forsøger at bruge systemet (i) ikke kan finde ud af om systemet tilbyder bestemte faciliteter (eksternt), (ii) ikke kan finde ud af hvorledes systemet er opbygget (internt), og (iii) ikke ved om han eller hun ved dette! Det sidste indebærer at et sikkert system ``bluffer'' ikke-autoriserede brugere -- for ellers ville de vide noget, hvormed de eventuelt kunne bryde systemets sikkerhed.
Store domæneanvendelser er i sig selv fysisk, dvs. geografisk vidt fordelt, og visse anvendelser benytter sig af sådan distribution for at sikre troværdighed.
Distribution er et svært forskningsområde, men det er vigtigt. Ved IT/DTU udforskes og undervises der i distribuerede systemer, bl.a. i forbindelse med næste emne.
Parallellisme er et centralt emne, især i forbindelse med distribuerede domæneanvendelser (generel parallellisme), men også i forbindelse med såkaldt massivt parallelle datamater (speciel parallellisme).
Der henvises iøvrigt til afsnit 3.1.2.
Generel parallelisme dyrkes intensivt ved IT/DTU: undervisnings- såvelsom forsknings-mæssigt (ved lektor Hans Henrik Løvengreen).
Generelt kan vi sige dette: ved konstruktion af parallelle programmelsystemer har det vist sig at man opnår de sikreste resultater ved at se bort fra hver enkel process' udførelseshastighed, herunder også hastighed af tilknyttet maskinel. At bero, i sin konstruktion, på absolutte tidsantagelser har vist sig at være en sikker vej til katastrofe: i projekter såvelsom i produkter.
Det forrige caveat bærer over også til nærværende deldisciplin. I indlejrede systemer, f.eks. i mikroinstrumenter, i medico-teknik, våbensystemer, process styring, mmm., spiller koordinering mellem maskinelle og programmelle -- de ``hårde'' og de ``bløde'' -- processer en altafgørende rolle for systemernes ydeevne.
Man skal ikke overse at et system er sandtidskritisk uanset om der er tale om milisekunders eller ti års reaktionstid (`response time').
Igen forskes og undervises der ihærdigt på dette område ved IT/DTU (ved bla. lektor Michael R. Hansen i tæt samarbejde med professor Zhou Chaochen, UNU/IIST).