Ders Adı Kodu Yarıyıl T+U Saat Kredi AKTS
Yazılım Mühendisliğinde Biçimsel Yöntemler SWE 302 6 3 + 0 3 5
Ön Koşul Dersleri
Önerilen Seçmeli Dersler
Dersin Dili İngilizce
Dersin Seviyesi Lisans
Dersin Türü Zorunlu
Dersin Koordinatörü Prof.Dr. DEVRİM AKGÜN
Dersi Verenler Prof.Dr. DEVRİM AKGÜN,
Dersin Yardımcıları
Dersin Kategorisi Diğer
Dersin Amacı

Formal ve formal olmayan yazılım geliştirme yöntemleri bilgisini kazanmak. Yazılım geliştirme döngüsünün başlangıç aşamalarına odaklanmak.

Dersin İçeriği

Propositional logic, predicate logic, quantifiers, hoare logic, weakest preconditions and strongest postconditions, recursion and terminations, inductive data types, lemmas and proofs, sorting algorithms, abstraction, and modules, invariants for data structures, loop invariants, specifications for recursive and iterative programs, specifications for objects

# Ders Öğrenme Çıktıları Öğretim Yöntemleri Ölçme Yöntemleri
1 Understand mathematical foundations of formal methods Anlatım, Soru-Cevap, Tartışma, Doğru Yanlış Testleri, Kısa Cevaplı Testler, Eşleştirme Testler,
2 Write formal specifications and contracts Anlatım, Soru-Cevap, Tartışma, Doğru Yanlış Testleri, Kısa Cevaplı Testler, Eşleştirme Testler,
3 Write code level verification and specification Anlatım, Soru-Cevap, Tartışma, Doğru Yanlış Testleri, Kısa Cevaplı Testler, Eşleştirme Testler,
Hafta Ders Konuları Ön Hazırlık
1 Introduction Weekly presentations
2 Propositional logic Weekly presentations
3 Predicate logic and quantifiers Weekly presentations
4 Hoare Logic, weakest preconditions and strongest postconditions Weekly presentations
5 Loop invariants Weekly presentations
6 Recursion and terminations, inductive data types Weekly presentations
7 Lemmas and proofs Weekly presentations
8 Midterm exam Weekly presentations
9 List proofs, sorting algorithms Weekly presentations
10 Abstraction and modules Weekly presentations
11 Invariants for data structures Weekly presentations
12 Specifications for recursive and iterative Programs Weekly presentations
13 Specifications for Objects Weekly presentations
14 Recent topics and project presentations Weekly presentations
Kaynaklar
Ders Notu

Haftalık yüklenen sunumlar

Ders Kaynakları

Leino, K. Rustan M. Program Proofs. MIT Press, 2023.

Daniel Jackson, Software Abstractions, MIT Press, 2006

https://dafny.org/dafny/

Sıra Program Çıktıları Katkı Düzeyi
1 2 3 4 5
1 Mühendislik Bilgisi: Matematik, fen bilimleri, temel mühendislik, bilgisayarla hesaplama ve ilgili mühendislik disiplinine özgü konularda bilgi; bu bilgileri, karmaşık mühendislik problemlerinin çözümünde kullanabilme becerisi. X
2 Problem Analizi: Karmaşık mühendislik problemlerini, temel bilim, matematik ve mühendislik bilgilerini kullanarak ve ele alınan problemle ilgili BM Sürdürülebilir Kalkınma Amaçlarını gözeterek tanımlama, formüle etme ve analiz becerisi. X
3 Mühendislik Tasarımı: Karmaşık mühendislik problemlerine yaratıcı çözümler tasarlama becerisi; karmaşık sistemleri, süreçleri, cihazları veya ürünleri gerçekçi kısıtları ve koşulları gözeterek, mevcut ve gelecekteki gereksinimleri karşılayacak biçimde tasarlama becerisi. X
4 Teknik ve Araçların Kullanımı: Karmaşık mühendislik problemlerinin analizi ve çözümüne yönelik, tahmin ve modelleme de dahil olmak üzere, uygun teknikleri, kaynakları ve modern mühendislik ve bilişim araçlarını, sınırlamalarının da farkında olarak seçme ve kullanma becerisi. X
5 Araştırma ve İnceleme: Karmaşık mühendislik problemlerinin incelenmesi için literatür araştırması, deney tasarlama, deney yapma, veri toplama, sonuçları analiz etme ve yorumlama dahil, araştırma yöntemlerini kullanma becerisi. X
6 Mühendislik Uygulamalarının Küresel Etkisi: Mühendislik uygulamalarının BM Sürdürülebilir Kalkınma Amaçları* kapsamında, topluma, sağlık ve güvenliğe, ekonomiye, sürdürülebilirlik ve çevreye etkileri hakkında bilgi; mühendislik çözümlerinin hukuksal sonuçları konusunda farkındalık.
7 Mühendislik Etiği: Mühendislik meslek ilkelerine* uygun davranma, etik sorumluluk hakkında bilgi; hiçbir konuda ayrımcılık yapmadan, tarafsız davranma ve çeşitliliği kapsayıcı olma konularında farkındalık.
8 Bireysel ve Takım Çalışması: Bireysel olarak ve disiplin içi ve çok disiplinli takımlarda (yüz yüze, uzaktan veya karma) takım üyesi veya lideri olarak etkin biçimde çalışabilme becerisi.
9 Sözlü ve Yazılı İletişim: Hedef kitlenin çeşitli farklılıklarını (eğitim, dil, meslek gibi) dikkate alarak, teknik konularda sözlü, yazılı etkin iletişim kurma becerisi.
10 Proje Yönetimi: Proje yönetimi ve ekonomik yapılabilirlik analizi gibi iş hayatındaki uygulamalar hakkında bilgi; girişimcilik ve yenilikçilik hakkında farkındalık.
11 Yaşam Boyu Öğrenme: Bağımsız ve sürekli öğrenebilme, yeni ve gelişmekte olan teknolojilere uyum sağlayabilme ve teknolojik değişimlerle ilgili sorgulayıcı düşünebilmeyi kapsayan yaşam boyu öğrenme becerisi.
# Ders Öğrenme Çıktılarının Program Çıktılarına Katkısı PÇ 1 PÇ 2 PÇ 3 PÇ 4 PÇ 5 PÇ 6 PÇ 7 PÇ 8 PÇ 9 PÇ 10 PÇ 11
1 Understand mathematical foundations of formal methods
2 Write formal specifications and contracts
3 Write code level verification and specification
Değerlendirme Sistemi
Yarıyıl Çalışmaları Katkı Oranı
1. Ara Sınav 70
1. Kısa Sınav 10
1. Ödev 10
1. Proje / Tasarım 10
Toplam 100
1. Final 50
1. Yıl İçinin Başarıya 50
Toplam 100
AKTS - İş Yükü Etkinlik Sayı Süre (Saat) Toplam İş Yükü (Saat)
Ders Süresi (Sınav haftası dahildir: 16x toplam ders saati) 16 3 48
Sınıf Dışı Ders Çalışma Süresi(Ön çalışma, pekiştirme) 16 3 48
Ara Sınav 1 10 10
Proje / Tasarım 1 6 6
Final 1 10 10
Ödev 2 2 4
Performans Görevi (Uygulama) 1 1 1
Toplam İş Yükü 127
Toplam İş Yükü / 25 (Saat) 5,08
dersAKTSKredisi 5