Abstrakt. Förväntningar (genomsnitt) egenskaper för kontinuerliga slumpvariabler används i stor utsträckning för att bedöma prestandaegenskaper inom ingenjörsvetenskap och fysik. I detta dokument presenteras en infrastruktur som kan användas för att formellt resonera om förväntade egenskaper hos de flesta av de kontinuerliga slumpvariablerna i ett teoremtest. Med utgångspunkt från den relativt komplexa högre-order-logiska definitionen av förväntan, baserat på Lebesgue integration, bekräftar vi formellt nyckelförväntningsegenskaper som gör att vi kan resonera om förväntningarna på en kontinuerlig slumpmässig variabel i termer av enkla aritmetiska operationer. För att illustrera den praktiska effektiviteten och utnyttjandet av vårt tillvägagångssätt presenterar vi också den formella verifieringen av förväntan egenskaper hos de allmänt använda kontinuerliga slumpvariabler: Enhetliga, Triangulära och Exponential.
Statistiska egenskaper hos kontinuerliga slumpvariabler har också verifierats i REF.
Formal Reasoning about Expectation Properties for Continuous Random Variables
{'venue': 'FM', 'journal': None, 'mag_field_of_study': ['Computer Science']}