Sadržaj

• Uvod
  • Neformalno ispitivanje ispravnosti programa
  • Osnovni pojmovi
    • Horove trojke
    • Uloga Horovih trojki u razvoju softvera
    • Algoritmi, pseudokod i dijagrami toka
  • Formalno ispitivanje ispravnosti programa
    
    
• Faktorijel
  • Specifikacija
  • Pseudokod programa
  • Testiranje programa
  • Invarijanta petlje
  • Dokaz parcijalne korektnosti programa
  • Dokaz zaustavljanja programa
  • Prevođenje u C program
  
  
• NZD
  • Specifikacija
  • Pseudokod programa
  • Testiranje programa
  • Invarijanta petlje
  • Dokaz parcijalne korektnosti programa
  • Dokaz zaustavljanja programa
  • Prevođenje u C program
  
  
• Celobrojno deljenje
  • Specifikacija
  • Pseudokod programa
  • Testiranje programa
  • Invarijanta petlje
  • Dokaz parcijalne korektnosti programa
  • Dokaz zaustavljanja programa
  • Prevođenje u C program
  
  
• Hardverdsko celobrojno deljenje
  • Specifikacija
  • Pseudokod programa
  • Invarijanta petlje (izvođenje iz brojača)
    • Izvođenje prve i druge invarijante
    • Pseudokod programa sa istaknutim invarijantama
  • Dokaz zaustavljanja programa
  • Prevođenje u C program
  
  
• Sortiranje niza - Selection sort
  • Specifikacija
  • Pseudokod programa
  • Testiranje programa
  • Invarijanta petlje
  • Dokaz parcijalne korektnosti programa
  • Dokaz zaustavljanja programa
  • Prevođenje u C program
  
  
• Korisni linkovi i materijali
• Literatura
• Sadržaj